:: YELLOW_1 semantic presentation

begin

registration
let L be Lattice;
cluster LattPOSet L ->  with_suprema with_infima ;
coherence
 ( LattPOSet L is with_suprema & LattPOSet L is with_infima ) by LATTICE3:11;
end;

registration
let L be upper-bounded Lattice;
cluster LattPOSet L ->  upper-bounded ;
coherence
 LattPOSet L is upper-bounded
proof
 ex x being Element of (LattPOSet L) st x is_>=_than the carrier of (LattPOSet L)
proof
take x = Top (LattPOSet L); ::_thesis: x is_>=_than the carrier of (LattPOSet L)
consider z being Element of L such that
A1: for v being Element of L holds
( z "\/" v = z & v "\/" z = z ) by LATTICES:def_14;
reconsider z9 = z as Element of (LattPOSet L) ;
A2: z = Top L by A1, LATTICES:def_17;
A3: now__::_thesis:_for_b9_being_Element_of_(LattPOSet_L)_st_b9_is_<=_than_{}_holds_
z9_>=_b9
let b9 be Element of (LattPOSet L); ::_thesis: ( b9 is_<=_than {} implies z9 >= b9 )
reconsider b = b9 as Element of L ;
assume  b9 is_<=_than {} ; ::_thesis: z9 >= b9
A4: ( b % = b & z % = z ) ;
 b [= z by A2, LATTICES:19;
hence  z9 >= b9 by A4, LATTICE3:7; ::_thesis: verum
end;
 z9 is_<=_than {} by YELLOW_0:6;
then A5: z9 = "/\" ({},(LattPOSet L)) by A3, YELLOW_0:31;
now__::_thesis:_for_a_being_Element_of_(LattPOSet_L)_st_a_in_the_carrier_of_(LattPOSet_L)_holds_
a_<=_x
reconsider x9 = x as Element of L ;
let a be Element of (LattPOSet L); ::_thesis: ( a in the carrier of (LattPOSet L) implies a <= x )
assume  a in the carrier of (LattPOSet L) ; ::_thesis: a <= x
reconsider a9 = a as Element of L ;
 Top (LattPOSet L) = Top L by A2, A5, YELLOW_0:def_12;
then A6: a9 [= x9 by LATTICES:19;
 ( a9 % = a9 & x9 % = x9 ) ;
hence  a <= x by A6, LATTICE3:7; ::_thesis: verum
end;
hence  x is_>=_than the carrier of (LattPOSet L) by LATTICE3:def_9; ::_thesis: verum
end;
hence  LattPOSet L is upper-bounded by YELLOW_0:def_5; ::_thesis: verum
end;
end;

registration
let L be lower-bounded Lattice;
cluster LattPOSet L ->  lower-bounded ;
coherence
 LattPOSet L is lower-bounded
proof
 ex x being Element of (LattPOSet L) st x is_<=_than the carrier of (LattPOSet L)
proof
take x = Bottom (LattPOSet L); ::_thesis: x is_<=_than the carrier of (LattPOSet L)
consider z being Element of L such that
A1: for v being Element of L holds
( z "/\" v = z & v "/\" z = z ) by LATTICES:def_13;
reconsider z9 = z as Element of (LattPOSet L) ;
A2: z = Bottom L by A1, LATTICES:def_16;
A3: now__::_thesis:_for_b9_being_Element_of_(LattPOSet_L)_st_b9_is_>=_than_{}_holds_
z9_<=_b9
let b9 be Element of (LattPOSet L); ::_thesis: ( b9 is_>=_than {} implies z9 <= b9 )
reconsider b = b9 as Element of L ;
assume  b9 is_>=_than {} ; ::_thesis: z9 <= b9
A4: ( b % = b & z % = z ) ;
 z [= b by A2, LATTICES:16;
hence  z9 <= b9 by A4, LATTICE3:7; ::_thesis: verum
end;
 z9 is_>=_than {} by YELLOW_0:6;
then A5: z9 = "\/" ({},(LattPOSet L)) by A3, YELLOW_0:30;
now__::_thesis:_for_a_being_Element_of_(LattPOSet_L)_st_a_in_the_carrier_of_(LattPOSet_L)_holds_
x_<=_a
reconsider x9 = x as Element of L ;
let a be Element of (LattPOSet L); ::_thesis: ( a in the carrier of (LattPOSet L) implies x <= a )
assume  a in the carrier of (LattPOSet L) ; ::_thesis: x <= a
reconsider a9 = a as Element of L ;
 Bottom (LattPOSet L) = Bottom L by A2, A5, YELLOW_0:def_11;
then A6: x9 [= a9 by LATTICES:16;
 ( a9 % = a9 & x9 % = x9 ) ;
hence  x <= a by A6, LATTICE3:7; ::_thesis: verum
end;
hence  x is_<=_than the carrier of (LattPOSet L) by LATTICE3:def_8; ::_thesis: verum
end;
hence  LattPOSet L is lower-bounded by YELLOW_0:def_4; ::_thesis: verum
end;
end;

registration
let L be complete Lattice;
cluster LattPOSet L ->  complete ;
coherence
 LattPOSet L is complete
proof
 for X being set ex a being Element of (LattPOSet L) st
( X is_<=_than a & ( for b being Element of (LattPOSet L) st X is_<=_than b holds
a <= b ) )
proof
let X be set ; ::_thesis: ex a being Element of (LattPOSet L) st
( X is_<=_than a & ( for b being Element of (LattPOSet L) st X is_<=_than b holds
a <= b ) )
take a = "\/" (X,(LattPOSet L)); ::_thesis: ( X is_<=_than a & ( for b being Element of (LattPOSet L) st X is_<=_than b holds
a <= b ) )
 X is_less_than "\/" (X,L) by LATTICE3:def_21;
then  X is_<=_than ("\/" (X,L)) % by LATTICE3:30;
hence  X is_<=_than a by YELLOW_0:29; ::_thesis: for b being Element of (LattPOSet L) st X is_<=_than b holds
a <= b
let b be Element of (LattPOSet L); ::_thesis: ( X is_<=_than b implies a <= b )
reconsider b9 = b as Element of L ;
assume  X is_<=_than b ; ::_thesis: a <= b
then  X is_<=_than b9 % ;
then  X is_less_than b9 by LATTICE3:30;
then A1: "\/" (X,L) [= b9 by LATTICE3:def_21;
 ( ("\/" (X,L)) % = a & b9 % = b ) by YELLOW_0:29;
hence  a <= b by A1, LATTICE3:7; ::_thesis: verum
end;
hence  LattPOSet L is complete by LATTICE3:def_12; ::_thesis: verum
end;
end;

definition
let X be set ;
:: original: RelIncl
redefine func RelIncl X ->  Order of X;
coherence
 RelIncl X is Order of X
proof
now__::_thesis:_for_x_being_set_st_x_in_RelIncl_X_holds_
x_in_[:X,X:]
let x be set ; ::_thesis: ( x in RelIncl X implies x in [:X,X:] )
assume A1: x in RelIncl X ; ::_thesis: x in [:X,X:]
then consider y, z being set  such that
A2: x = [y,z] by RELAT_1:def_1;
 z in field (RelIncl X) by A1, A2, RELAT_1:15;
then A3: z in X by WELLORD2:def_1;
 y in field (RelIncl X) by A1, A2, RELAT_1:15;
then  y in X by WELLORD2:def_1;
hence  x in [:X,X:] by A2, A3, ZFMISC_1:87; ::_thesis: verum
end;
then reconsider R = RelIncl X as Relation of X by TARSKI:def_3;
 ( field R = X & R is reflexive ) by WELLORD2:def_1;
then  R is_reflexive_in X by RELAT_2:def_9;
then  dom R = X by ORDERS_1:13;
hence  RelIncl X is Order of X by PARTFUN1:def_2; ::_thesis: verum
end;
end;

definition
let X be set ;
func InclPoset X ->  strict RelStr  equals :: YELLOW_1:def 1
 RelStr(# X,(RelIncl X) #);
correctness
coherence
RelStr(# X,(RelIncl X) #) is strict RelStr ;
;
end;

:: deftheorem  defines InclPoset YELLOW_1:def_1_:_
 for X being set holds InclPoset X = RelStr(# X,(RelIncl X) #);

registration
let X be set ;
cluster InclPoset X ->  strict reflexive transitive antisymmetric ;
coherence
 ( InclPoset X is reflexive & InclPoset X is antisymmetric & InclPoset X is transitive ) ;
end;

registration
let X be non empty set ;
cluster InclPoset X ->  non empty strict ;
coherence
 not InclPoset X is empty ;
end;

theorem :: YELLOW_1:1
for X being set holds
( the carrier of (InclPoset X) = X & the InternalRel of (InclPoset X) = RelIncl X ) ;

definition
let X be set ;
func BoolePoset X ->  strict RelStr  equals :: YELLOW_1:def 2
 LattPOSet (BooleLatt X);
correctness
coherence
LattPOSet (BooleLatt X) is strict RelStr ;
;
end;

:: deftheorem  defines BoolePoset YELLOW_1:def_2_:_
 for X being set holds BoolePoset X = LattPOSet (BooleLatt X);

registration
let X be set ;
cluster BoolePoset X ->  non empty strict reflexive transitive antisymmetric ;
coherence
 ( not BoolePoset X is empty & BoolePoset X is reflexive & BoolePoset X is antisymmetric & BoolePoset X is transitive ) ;
end;

registration
let X be set ;
cluster BoolePoset X ->  strict complete ;
coherence
 BoolePoset X is complete ;
end;

theorem Th2: :: YELLOW_1:2
for X being set
for x, y being Element of (BoolePoset X) holds
( x <= y iff x c= y )
proof
let X be set ; ::_thesis: for x, y being Element of (BoolePoset X) holds
( x <= y iff x c= y )
let x, y be Element of (BoolePoset X); ::_thesis: ( x <= y iff x c= y )
reconsider x9 = x, y9 = y as Element of (BooleLatt X) ;
thus  ( x <= y implies x c= y ) ::_thesis: ( x c= y implies x <= y )
proof
assume  x <= y ; ::_thesis: x c= y
then  x9 % <= y9 % ;
then  x9 [= y9 by LATTICE3:7;
hence  x c= y by LATTICE3:2; ::_thesis: verum
end;
assume  x c= y ; ::_thesis: x <= y
then  x9 [= y9 by LATTICE3:2;
then  x9 % <= y9 % by LATTICE3:7;
hence  x <= y ; ::_thesis: verum
end;

theorem Th3: :: YELLOW_1:3
for X being non empty set
for x, y being Element of (InclPoset X) holds
( x <= y iff x c= y )
proof
let X be non empty set ; ::_thesis: for x, y being Element of (InclPoset X) holds
( x <= y iff x c= y )
let x, y be Element of (InclPoset X); ::_thesis: ( x <= y iff x c= y )
thus  ( x <= y implies x c= y ) ::_thesis: ( x c= y implies x <= y )
proof
assume  x <= y ; ::_thesis: x c= y
then  [x,y] in the InternalRel of (InclPoset X) by ORDERS_2:def_5;
hence  x c= y by WELLORD2:def_1; ::_thesis: verum
end;
thus  ( x c= y implies x <= y ) ::_thesis: verum
proof
assume  x c= y ; ::_thesis: x <= y
then  [x,y] in RelIncl X by WELLORD2:def_1;
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
end;

theorem Th4: :: YELLOW_1:4
for X being set holds BoolePoset X = InclPoset (bool X)
proof
let X be set ; ::_thesis: BoolePoset X = InclPoset (bool X)
set B = BoolePoset X;
 the carrier of (BoolePoset X) = bool X by LATTICE3:def_1;
then reconsider In = the InternalRel of (BoolePoset X) as Relation of (bool X) ;
 for x being set st x in bool X holds
ex y being set st [x,y] in In
proof
let x be set ; ::_thesis: ( x in bool X implies ex y being set st [x,y] in In )
assume  x in bool X ; ::_thesis: ex y being set st [x,y] in In
then reconsider x9 = x as Element of (BoolePoset X) by LATTICE3:def_1;
take y = x9; ::_thesis: [x,y] in In
 x9 <= y ;
hence  [x,y] in In by ORDERS_2:def_5; ::_thesis: verum
end;
then A1: dom In = bool X by RELSET_1:9;
A2: now__::_thesis:_for_Y,_Z_being_set_st_Y_in_bool_X_&_Z_in_bool_X_holds_
(_(_[Y,Z]_in_the_InternalRel_of_(BoolePoset_X)_implies_Y_c=_Z_)_&_(_Y_c=_Z_implies_[Y,Z]_in_the_InternalRel_of_(BoolePoset_X)_)_)
let Y, Z be set ; ::_thesis: ( Y in bool X & Z in bool X implies ( ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) ) )
assume  ( Y in bool X & Z in bool X ) ; ::_thesis: ( ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) )
then reconsider Y9 = Y, Z9 = Z as Element of (BoolePoset X) by LATTICE3:def_1;
thus  ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) ::_thesis: ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) )
proof
assume  [Y,Z] in the InternalRel of (BoolePoset X) ; ::_thesis: Y c= Z
then  Y9 <= Z9 by ORDERS_2:def_5;
hence  Y c= Z by Th2; ::_thesis: verum
end;
thus  ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) ::_thesis: verum
proof
assume  Y c= Z ; ::_thesis: [Y,Z] in the InternalRel of (BoolePoset X)
then  Y9 <= Z9 by Th2;
hence  [Y,Z] in the InternalRel of (BoolePoset X) by ORDERS_2:def_5; ::_thesis: verum
end;
end;
 for y being set st y in bool X holds
ex x being set st [x,y] in In
proof
let y be set ; ::_thesis: ( y in bool X implies ex x being set st [x,y] in In )
assume  y in bool X ; ::_thesis: ex x being set st [x,y] in In
then reconsider y9 = y as Element of (BoolePoset X) by LATTICE3:def_1;
take x = y9; ::_thesis: [x,y] in In
 x <= y9 ;
hence  [x,y] in In by ORDERS_2:def_5; ::_thesis: verum
end;
then  field the InternalRel of (BoolePoset X) = (bool X) \/ (bool X) by A1, RELSET_1:10;
then  the InternalRel of (BoolePoset X) = RelIncl (bool X) by A2, WELLORD2:def_1;
hence  BoolePoset X = InclPoset (bool X) by LATTICE3:def_1; ::_thesis: verum
end;

theorem :: YELLOW_1:5
for X being set
for Y being Subset-Family of X holds InclPoset Y is full SubRelStr of BoolePoset X
proof
let X be set ; ::_thesis: for Y being Subset-Family of X holds InclPoset Y is full SubRelStr of BoolePoset X
set L = BoolePoset X;
let Y be Subset-Family of X; ::_thesis: InclPoset Y is full SubRelStr of BoolePoset X
reconsider Y9 = Y as Subset of (BoolePoset X) by LATTICE3:def_1;
 the carrier of (BoolePoset X) = bool X by LATTICE3:def_1;
then reconsider In = the InternalRel of (BoolePoset X) as Relation of (bool X) ;
 for x being set st x in bool X holds
ex y being set st [x,y] in In
proof
let x be set ; ::_thesis: ( x in bool X implies ex y being set st [x,y] in In )
assume  x in bool X ; ::_thesis: ex y being set st [x,y] in In
then reconsider x9 = x as Element of (BoolePoset X) by LATTICE3:def_1;
take y = x9; ::_thesis: [x,y] in In
 x9 <= y ;
hence  [x,y] in In by ORDERS_2:def_5; ::_thesis: verum
end;
then A1: dom In = bool X by RELSET_1:9;
A2: now__::_thesis:_for_Y,_Z_being_set_st_Y_in_bool_X_&_Z_in_bool_X_holds_
(_(_[Y,Z]_in_the_InternalRel_of_(BoolePoset_X)_implies_Y_c=_Z_)_&_(_Y_c=_Z_implies_[Y,Z]_in_the_InternalRel_of_(BoolePoset_X)_)_)
let Y, Z be set ; ::_thesis: ( Y in bool X & Z in bool X implies ( ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) ) )
assume  ( Y in bool X & Z in bool X ) ; ::_thesis: ( ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) )
then reconsider Y9 = Y, Z9 = Z as Element of (BoolePoset X) by LATTICE3:def_1;
thus  ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) ::_thesis: ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) )
proof
assume  [Y,Z] in the InternalRel of (BoolePoset X) ; ::_thesis: Y c= Z
then  Y9 <= Z9 by ORDERS_2:def_5;
hence  Y c= Z by Th2; ::_thesis: verum
end;
thus  ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) ::_thesis: verum
proof
assume  Y c= Z ; ::_thesis: [Y,Z] in the InternalRel of (BoolePoset X)
then  Y9 <= Z9 by Th2;
hence  [Y,Z] in the InternalRel of (BoolePoset X) by ORDERS_2:def_5; ::_thesis: verum
end;
end;
 for y being set st y in bool X holds
ex x being set st [x,y] in In
proof
let y be set ; ::_thesis: ( y in bool X implies ex x being set st [x,y] in In )
assume  y in bool X ; ::_thesis: ex x being set st [x,y] in In
then reconsider y9 = y as Element of (BoolePoset X) by LATTICE3:def_1;
take x = y9; ::_thesis: [x,y] in In
 x <= y9 ;
hence  [x,y] in In by ORDERS_2:def_5; ::_thesis: verum
end;
then  field the InternalRel of (BoolePoset X) = (bool X) \/ (bool X) by A1, RELSET_1:10;
then A3: the InternalRel of (BoolePoset X) = RelIncl (bool X) by A2, WELLORD2:def_1;
 RelStr(# Y9,( the InternalRel of (BoolePoset X) |_2 Y9) #) is full SubRelStr of BoolePoset X by YELLOW_0:56;
hence  InclPoset Y is full SubRelStr of BoolePoset X by A3, WELLORD2:7; ::_thesis: verum
end;

theorem :: YELLOW_1:6
for X being non empty set st InclPoset X is with_suprema holds
for x, y being Element of (InclPoset X) holds x \/ y c= x "\/" y
proof
let X be non empty set ; ::_thesis: ( InclPoset X is with_suprema implies for x, y being Element of (InclPoset X) holds x \/ y c= x "\/" y )
assume A1: InclPoset X is with_suprema ; ::_thesis: for x, y being Element of (InclPoset X) holds x \/ y c= x "\/" y
let x, y be Element of (InclPoset X); ::_thesis: x \/ y c= x "\/" y
 y <= x "\/" y by A1, YELLOW_0:22;
then A2: y c= x "\/" y by Th3;
 x <= x "\/" y by A1, YELLOW_0:22;
then  x c= x "\/" y by Th3;
hence  x \/ y c= x "\/" y by A2, XBOOLE_1:8; ::_thesis: verum
end;

theorem :: YELLOW_1:7
for X being non empty set st InclPoset X is with_infima holds
for x, y being Element of (InclPoset X) holds x "/\" y c= x /\ y
proof
let X be non empty set ; ::_thesis: ( InclPoset X is with_infima implies for x, y being Element of (InclPoset X) holds x "/\" y c= x /\ y )
assume A1: InclPoset X is with_infima ; ::_thesis: for x, y being Element of (InclPoset X) holds x "/\" y c= x /\ y
let x, y be Element of (InclPoset X); ::_thesis: x "/\" y c= x /\ y
 x "/\" y <= y by A1, YELLOW_0:23;
then A2: x "/\" y c= y by Th3;
 x "/\" y <= x by A1, YELLOW_0:23;
then  x "/\" y c= x by Th3;
hence  x "/\" y c= x /\ y by A2, XBOOLE_1:19; ::_thesis: verum
end;

theorem Th8: :: YELLOW_1:8
for X being non empty set
for x, y being Element of (InclPoset X) st x \/ y in X holds
x "\/" y = x \/ y
proof
let X be non empty set ; ::_thesis: for x, y being Element of (InclPoset X) st x \/ y in X holds
x "\/" y = x \/ y
let x, y be Element of (InclPoset X); ::_thesis: ( x \/ y in X implies x "\/" y = x \/ y )
assume  x \/ y in X ; ::_thesis: x "\/" y = x \/ y
then reconsider z = x \/ y as Element of (InclPoset X) ;
 y c= z by XBOOLE_1:7;
then A1: y <= z by Th3;
A2: now__::_thesis:_for_c_being_Element_of_(InclPoset_X)_st_x_<=_c_&_y_<=_c_holds_
z_<=_c
let c be Element of (InclPoset X); ::_thesis: ( x <= c & y <= c implies z <= c )
assume  ( x <= c & y <= c ) ; ::_thesis: z <= c
then  ( x c= c & y c= c ) by Th3;
then  z c= c by XBOOLE_1:8;
hence  z <= c by Th3; ::_thesis: verum
end;
 x c= z by XBOOLE_1:7;
then  x <= z by Th3;
hence  x "\/" y = x \/ y by A1, A2, LATTICE3:def_13; ::_thesis: verum
end;

theorem Th9: :: YELLOW_1:9
for X being non empty set
for x, y being Element of (InclPoset X) st x /\ y in X holds
x "/\" y = x /\ y
proof
let X be non empty set ; ::_thesis: for x, y being Element of (InclPoset X) st x /\ y in X holds
x "/\" y = x /\ y
let x, y be Element of (InclPoset X); ::_thesis: ( x /\ y in X implies x "/\" y = x /\ y )
assume  x /\ y in X ; ::_thesis: x "/\" y = x /\ y
then reconsider z = x /\ y as Element of (InclPoset X) ;
 z c= y by XBOOLE_1:17;
then A1: z <= y by Th3;
A2: now__::_thesis:_for_c_being_Element_of_(InclPoset_X)_st_c_<=_x_&_c_<=_y_holds_
c_<=_z
let c be Element of (InclPoset X); ::_thesis: ( c <= x & c <= y implies c <= z )
assume  ( c <= x & c <= y ) ; ::_thesis: c <= z
then  ( c c= x & c c= y ) by Th3;
then  c c= z by XBOOLE_1:19;
hence  c <= z by Th3; ::_thesis: verum
end;
 z c= x by XBOOLE_1:17;
then  z <= x by Th3;
hence  x "/\" y = x /\ y by A1, A2, LATTICE3:def_14; ::_thesis: verum
end;

theorem :: YELLOW_1:10
for L being RelStr st ( for x, y being Element of L holds
( x <= y iff x c= y ) ) holds
the InternalRel of L = RelIncl the carrier of L
proof
let L be RelStr ; ::_thesis: ( ( for x, y being Element of L holds
( x <= y iff x c= y ) ) implies the InternalRel of L = RelIncl the carrier of L )
assume A1: for x, y being Element of L holds
( x <= y iff x c= y ) ; ::_thesis: the InternalRel of L = RelIncl the carrier of L
A2: now__::_thesis:_for_Y,_Z_being_set_st_Y_in_the_carrier_of_L_&_Z_in_the_carrier_of_L_holds_
(_(_[Y,Z]_in_the_InternalRel_of_L_implies_Y_c=_Z_)_&_(_Y_c=_Z_implies_[Y,Z]_in_the_InternalRel_of_L_)_)
let Y, Z be set ; ::_thesis: ( Y in the carrier of L & Z in the carrier of L implies ( ( [Y,Z] in the InternalRel of L implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of L ) ) )
assume  ( Y in the carrier of L & Z in the carrier of L ) ; ::_thesis: ( ( [Y,Z] in the InternalRel of L implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of L ) )
then reconsider Y9 = Y, Z9 = Z as Element of L ;
thus  ( [Y,Z] in the InternalRel of L implies Y c= Z ) ::_thesis: ( Y c= Z implies [Y,Z] in the InternalRel of L )
proof
assume  [Y,Z] in the InternalRel of L ; ::_thesis: Y c= Z
then  Y9 <= Z9 by ORDERS_2:def_5;
hence  Y c= Z by A1; ::_thesis: verum
end;
thus  ( Y c= Z implies [Y,Z] in the InternalRel of L ) ::_thesis: verum
proof
assume  Y c= Z ; ::_thesis: [Y,Z] in the InternalRel of L
then  Y9 <= Z9 by A1;
hence  [Y,Z] in the InternalRel of L by ORDERS_2:def_5; ::_thesis: verum
end;
end;
 for x being set st x in the carrier of L holds
ex y being set st [x,y] in the InternalRel of L
proof
let x be set ; ::_thesis: ( x in the carrier of L implies ex y being set st [x,y] in the InternalRel of L )
assume  x in the carrier of L ; ::_thesis: ex y being set st [x,y] in the InternalRel of L
then reconsider x9 = x as Element of L ;
take y = x9; ::_thesis: [x,y] in the InternalRel of L
 x9 <= y by A1;
hence  [x,y] in the InternalRel of L by ORDERS_2:def_5; ::_thesis: verum
end;
then A3: dom the InternalRel of L = the carrier of L by RELSET_1:9;
 for y being set st y in the carrier of L holds
ex x being set st [x,y] in the InternalRel of L
proof
let y be set ; ::_thesis: ( y in the carrier of L implies ex x being set st [x,y] in the InternalRel of L )
assume  y in the carrier of L ; ::_thesis: ex x being set st [x,y] in the InternalRel of L
then reconsider y9 = y as Element of L ;
take x = y9; ::_thesis: [x,y] in the InternalRel of L
 x <= y9 by A1;
hence  [x,y] in the InternalRel of L by ORDERS_2:def_5; ::_thesis: verum
end;
then  field the InternalRel of L = the carrier of L \/ the carrier of L by A3, RELSET_1:10;
hence  the InternalRel of L = RelIncl the carrier of L by A2, WELLORD2:def_1; ::_thesis: verum
end;

theorem :: YELLOW_1:11
for X being non empty set st ( for x, y being set st x in X & y in X holds
x \/ y in X ) holds
InclPoset X is with_suprema
proof
let X be non empty set ; ::_thesis: ( ( for x, y being set st x in X & y in X holds
x \/ y in X ) implies InclPoset X is with_suprema )
set L = InclPoset X;
assume A1: for x, y being set st x in X & y in X holds
x \/ y in X ; ::_thesis: InclPoset X is with_suprema
now__::_thesis:_for_a,_b_being_Element_of_(InclPoset_X)_holds_ex_sup_of_{a,b},_InclPoset_X
let a, b be Element of (InclPoset X); ::_thesis: ex_sup_of {a,b}, InclPoset X
 ex c being Element of (InclPoset X) st
( {a,b} is_<=_than c & ( for d being Element of (InclPoset X) st {a,b} is_<=_than d holds
c <= d ) )
proof
take c = a "\/" b; ::_thesis: ( {a,b} is_<=_than c & ( for d being Element of (InclPoset X) st {a,b} is_<=_than d holds
c <= d ) )
A2: a \/ b = c by A1, Th8;
then  b c= c by XBOOLE_1:7;
then A3: b <= c by Th3;
 a c= c by A2, XBOOLE_1:7;
then  a <= c by Th3;
hence  {a,b} is_<=_than c by A3, YELLOW_0:8; ::_thesis: for d being Element of (InclPoset X) st {a,b} is_<=_than d holds
c <= d
let d be Element of (InclPoset X); ::_thesis: ( {a,b} is_<=_than d implies c <= d )
assume A4: {a,b} is_<=_than d ; ::_thesis: c <= d
 b in {a,b} by TARSKI:def_2;
then  b <= d by A4, LATTICE3:def_9;
then A5: b c= d by Th3;
 a in {a,b} by TARSKI:def_2;
then  a <= d by A4, LATTICE3:def_9;
then  a c= d by Th3;
then  a \/ b c= d by A5, XBOOLE_1:8;
then  c c= d by A1, Th8;
hence  c <= d by Th3; ::_thesis: verum
end;
hence  ex_sup_of {a,b}, InclPoset X by YELLOW_0:15; ::_thesis: verum
end;
hence  InclPoset X is with_suprema by YELLOW_0:20; ::_thesis: verum
end;

theorem :: YELLOW_1:12
for X being non empty set st ( for x, y being set st x in X & y in X holds
x /\ y in X ) holds
InclPoset X is with_infima
proof
let X be non empty set ; ::_thesis: ( ( for x, y being set st x in X & y in X holds
x /\ y in X ) implies InclPoset X is with_infima )
set L = InclPoset X;
assume A1: for x, y being set st x in X & y in X holds
x /\ y in X ; ::_thesis: InclPoset X is with_infima
now__::_thesis:_for_a,_b_being_Element_of_(InclPoset_X)_holds_ex_inf_of_{a,b},_InclPoset_X
let a, b be Element of (InclPoset X); ::_thesis: ex_inf_of {a,b}, InclPoset X
 ex c being Element of (InclPoset X) st
( {a,b} is_>=_than c & ( for d being Element of (InclPoset X) st {a,b} is_>=_than d holds
c >= d ) )
proof
take c = a "/\" b; ::_thesis: ( {a,b} is_>=_than c & ( for d being Element of (InclPoset X) st {a,b} is_>=_than d holds
c >= d ) )
A2: a /\ b = c by A1, Th9;
then  c c= b by XBOOLE_1:17;
then A3: c <= b by Th3;
 c c= a by A2, XBOOLE_1:17;
then  c <= a by Th3;
hence  {a,b} is_>=_than c by A3, YELLOW_0:8; ::_thesis: for d being Element of (InclPoset X) st {a,b} is_>=_than d holds
c >= d
let d be Element of (InclPoset X); ::_thesis: ( {a,b} is_>=_than d implies c >= d )
assume A4: {a,b} is_>=_than d ; ::_thesis: c >= d
 b in {a,b} by TARSKI:def_2;
then  d <= b by A4, LATTICE3:def_8;
then A5: d c= b by Th3;
 a in {a,b} by TARSKI:def_2;
then  d <= a by A4, LATTICE3:def_8;
then  d c= a by Th3;
then  d c= a /\ b by A5, XBOOLE_1:19;
then  d c= c by A1, Th9;
hence  c >= d by Th3; ::_thesis: verum
end;
hence  ex_inf_of {a,b}, InclPoset X by YELLOW_0:16; ::_thesis: verum
end;
hence  InclPoset X is with_infima by YELLOW_0:21; ::_thesis: verum
end;

theorem Th13: :: YELLOW_1:13
for X being non empty set st {} in X holds
Bottom (InclPoset X) = {}
proof
let X be non empty set ; ::_thesis: ( {} in X implies Bottom (InclPoset X) = {} )
assume  {} in X ; ::_thesis: Bottom (InclPoset X) = {}
then reconsider a = {} as Element of (InclPoset X) ;
now__::_thesis:_for_b_being_Element_of_(InclPoset_X)_st_b_in_X_holds_
a_<=_b
let b be Element of (InclPoset X); ::_thesis: ( b in X implies a <= b )
assume  b in X ; ::_thesis: a <= b
 {} c= b by XBOOLE_1:2;
hence  a <= b by Th3; ::_thesis: verum
end;
then  a is_<=_than X by LATTICE3:def_8;
then  InclPoset X is lower-bounded by YELLOW_0:def_4;
then  ( {} is_<=_than a & ex_sup_of {} , InclPoset X ) by YELLOW_0:6, YELLOW_0:42;
then  "\/" ({},(InclPoset X)) <= a by YELLOW_0:def_9;
then A1: "\/" ({},(InclPoset X)) c= a by Th3;
thus  Bottom (InclPoset X) = "\/" ({},(InclPoset X)) by YELLOW_0:def_11
.= {} by A1 ; ::_thesis: verum
end;

theorem Th14: :: YELLOW_1:14
for X being non empty set st union X in X holds
Top (InclPoset X) = union X
proof
let X be non empty set ; ::_thesis: ( union X in X implies Top (InclPoset X) = union X )
assume  union X in X ; ::_thesis: Top (InclPoset X) = union X
then reconsider a = union X as Element of (InclPoset X) ;
now__::_thesis:_for_b_being_Element_of_(InclPoset_X)_st_b_in_X_holds_
b_<=_a
let b be Element of (InclPoset X); ::_thesis: ( b in X implies b <= a )
assume  b in X ; ::_thesis: b <= a
 b c= union X by ZFMISC_1:74;
hence  b <= a by Th3; ::_thesis: verum
end;
then  a is_>=_than X by LATTICE3:def_9;
then  InclPoset X is upper-bounded by YELLOW_0:def_5;
then  ( {} is_>=_than a & ex_inf_of {} , InclPoset X ) by YELLOW_0:6, YELLOW_0:43;
then  a <= "/\" ({},(InclPoset X)) by YELLOW_0:def_10;
then A1: ( "/\" ({},(InclPoset X)) c= a & a c= "/\" ({},(InclPoset X)) ) by Th3, ZFMISC_1:74;
thus  Top (InclPoset X) = "/\" ({},(InclPoset X)) by YELLOW_0:def_12
.= union X by A1, XBOOLE_0:def_10 ; ::_thesis: verum
end;

theorem :: YELLOW_1:15
for X being non empty set st InclPoset X is upper-bounded holds
union X in X
proof
let X be non empty set ; ::_thesis: ( InclPoset X is upper-bounded implies union X in X )
assume  InclPoset X is upper-bounded ; ::_thesis: union X in X
then consider x being Element of (InclPoset X) such that
A1: x is_>=_than the carrier of (InclPoset X) by YELLOW_0:def_5;
now__::_thesis:_for_y_being_set_st_y_in_union_X_holds_
y_in_x
let y be set ; ::_thesis: ( y in union X implies y in x )
assume  y in union X ; ::_thesis: y in x
then consider Y being set  such that
A2: y in Y and
A3: Y in X by TARSKI:def_4;
reconsider Y = Y as Element of (InclPoset X) by A3;
 Y <= x by A1, LATTICE3:def_9;
then  Y c= x by Th3;
hence  y in x by A2; ::_thesis: verum
end;
then A4: union X c= x by TARSKI:def_3;
 ( x in X & x c= union X ) by ZFMISC_1:74;
hence  union X in X by A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: YELLOW_1:16
for X being non empty set st InclPoset X is lower-bounded holds
meet X in X
proof
let X be non empty set ; ::_thesis: ( InclPoset X is lower-bounded implies meet X in X )
assume  InclPoset X is lower-bounded ; ::_thesis: meet X in X
then consider x being Element of (InclPoset X) such that
A1: x is_<=_than the carrier of (InclPoset X) by YELLOW_0:def_4;
now__::_thesis:_for_y_being_set_st_y_in_x_holds_
y_in_meet_X
let y be set ; ::_thesis: ( y in x implies y in meet X )
assume A2: y in x ; ::_thesis: y in meet X
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
y_in_Y
let Y be set ; ::_thesis: ( Y in X implies y in Y )
assume  Y in X ; ::_thesis: y in Y
then reconsider Y9 = Y as Element of (InclPoset X) ;
 x <= Y9 by A1, LATTICE3:def_8;
then  x c= Y by Th3;
hence  y in Y by A2; ::_thesis: verum
end;
hence  y in meet X by SETFAM_1:def_1; ::_thesis: verum
end;
then A3: x c= meet X by TARSKI:def_3;
 ( x in X & meet X c= x ) by SETFAM_1:3;
hence  meet X in X by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

Lm1:  for X being set
for x, y being Element of (BoolePoset X) holds
( x /\ y in bool X & x \/ y in bool X )
proof
let X be set ; ::_thesis: for x, y being Element of (BoolePoset X) holds
( x /\ y in bool X & x \/ y in bool X )
let x, y be Element of (BoolePoset X); ::_thesis: ( x /\ y in bool X & x \/ y in bool X )
 x in the carrier of (BoolePoset X) ;
then A1: x in bool X by LATTICE3:def_1;
then  x /\ y c= X by XBOOLE_1:108;
hence  x /\ y in bool X ; ::_thesis: x \/ y in bool X
 y in the carrier of (BoolePoset X) ;
then  y in bool X by LATTICE3:def_1;
then  x \/ y c= X by A1, XBOOLE_1:8;
hence  x \/ y in bool X ; ::_thesis: verum
end;

theorem :: YELLOW_1:17
for X being set
for x, y being Element of (BoolePoset X) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y )
proof
let X be set ; ::_thesis: for x, y being Element of (BoolePoset X) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y )
let x, y be Element of (BoolePoset X); ::_thesis: ( x "\/" y = x \/ y & x "/\" y = x /\ y )
reconsider x = x, y = y as Element of (InclPoset (bool X)) by Th4;
 ( x "/\" y = x /\ y & x "\/" y = x \/ y ) by Lm1, Th8, Th9;
hence  ( x "\/" y = x \/ y & x "/\" y = x /\ y ) by Th4; ::_thesis: verum
end;

theorem :: YELLOW_1:18
for X being set holds Bottom (BoolePoset X) = {}
proof
let X be set ; ::_thesis: Bottom (BoolePoset X) = {}
thus  Bottom (BoolePoset X) = "\/" ({},(LattPOSet (BooleLatt X))) by YELLOW_0:def_11
.= "\/" ({},(BooleLatt X)) by YELLOW_0:29
.= Bottom (BooleLatt X) by LATTICE3:49
.= {} by LATTICE3:3 ; ::_thesis: verum
end;

theorem :: YELLOW_1:19
for X being set holds Top (BoolePoset X) = X
proof
let X be set ; ::_thesis: Top (BoolePoset X) = X
A1: Top (InclPoset (bool X)) = union (bool X) by Th14;
 BoolePoset X = InclPoset (bool X) by Th4;
hence  Top (BoolePoset X) = X by A1, ZFMISC_1:81; ::_thesis: verum
end;

theorem :: YELLOW_1:20
for X being set
for Y being non empty Subset of (BoolePoset X) holds inf Y = meet Y
proof
let X be set ; ::_thesis: for Y being non empty Subset of (BoolePoset X) holds inf Y = meet Y
set L = BoolePoset X;
let Y be non empty Subset of (BoolePoset X); ::_thesis: inf Y = meet Y
set y = the Element of Y;
A1: the carrier of (BoolePoset X) = bool X by LATTICE3:def_1;
then  the Element of Y c= X ;
then reconsider Me = meet Y as Element of (BoolePoset X) by A1, SETFAM_1:7;
A2: now__::_thesis:_for_b_being_Element_of_(BoolePoset_X)_st_b_is_<=_than_Y_holds_
Me_>=_b
let b be Element of (BoolePoset X); ::_thesis: ( b is_<=_than Y implies Me >= b )
assume A3: b is_<=_than Y ; ::_thesis: Me >= b
now__::_thesis:_for_Z_being_set_st_Z_in_Y_holds_
b_c=_Z
let Z be set ; ::_thesis: ( Z in Y implies b c= Z )
assume A4: Z in Y ; ::_thesis: b c= Z
then reconsider Z9 = Z as Element of (BoolePoset X) ;
 b <= Z9 by A3, A4, LATTICE3:def_8;
hence  b c= Z by Th2; ::_thesis: verum
end;
then  b c= Me by SETFAM_1:5;
hence  Me >= b by Th2; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_(BoolePoset_X)_st_b_in_Y_holds_
Me_<=_b
let b be Element of (BoolePoset X); ::_thesis: ( b in Y implies Me <= b )
assume  b in Y ; ::_thesis: Me <= b
then  Me c= b by SETFAM_1:3;
hence  Me <= b by Th2; ::_thesis: verum
end;
then  Me is_<=_than Y by LATTICE3:def_8;
hence  inf Y = meet Y by A2, YELLOW_0:33; ::_thesis: verum
end;

theorem :: YELLOW_1:21
for X being set
for Y being Subset of (BoolePoset X) holds sup Y = union Y
proof
let X be set ; ::_thesis: for Y being Subset of (BoolePoset X) holds sup Y = union Y
set L = BoolePoset X;
let Y be Subset of (BoolePoset X); ::_thesis: sup Y = union Y
A1: the carrier of (BoolePoset X) = bool X by LATTICE3:def_1;
then  union Y c= union (bool X) by ZFMISC_1:77;
then reconsider Un = union Y as Element of (BoolePoset X) by A1, ZFMISC_1:81;
A2: now__::_thesis:_for_b_being_Element_of_(BoolePoset_X)_st_b_is_>=_than_Y_holds_
Un_<=_b
let b be Element of (BoolePoset X); ::_thesis: ( b is_>=_than Y implies Un <= b )
assume A3: b is_>=_than Y ; ::_thesis: Un <= b
now__::_thesis:_for_Z_being_set_st_Z_in_Y_holds_
Z_c=_b
let Z be set ; ::_thesis: ( Z in Y implies Z c= b )
assume A4: Z in Y ; ::_thesis: Z c= b
then reconsider Z9 = Z as Element of (BoolePoset X) ;
 Z9 <= b by A3, A4, LATTICE3:def_9;
hence  Z c= b by Th2; ::_thesis: verum
end;
then  Un c= b by ZFMISC_1:76;
hence  Un <= b by Th2; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_(BoolePoset_X)_st_b_in_Y_holds_
b_<=_Un
let b be Element of (BoolePoset X); ::_thesis: ( b in Y implies b <= Un )
assume  b in Y ; ::_thesis: b <= Un
then  b c= Un by ZFMISC_1:74;
hence  b <= Un by Th2; ::_thesis: verum
end;
then  Un is_>=_than Y by LATTICE3:def_9;
hence  sup Y = union Y by A2, YELLOW_0:30; ::_thesis: verum
end;

theorem :: YELLOW_1:22
for T being non empty TopSpace
for X being Subset of (InclPoset the topology of T) holds sup X = union X
proof
let T be non empty TopSpace; ::_thesis: for X being Subset of (InclPoset the topology of T) holds sup X = union X
set L = InclPoset the topology of T;
let X be Subset of (InclPoset the topology of T); ::_thesis: sup X = union X
reconsider X = X as Subset-Family of T by XBOOLE_1:1;
reconsider Un = union X as Element of (InclPoset the topology of T) by PRE_TOPC:def_1;
A1: now__::_thesis:_for_b_being_Element_of_(InclPoset_the_topology_of_T)_st_b_is_>=_than_X_holds_
Un_<=_b
let b be Element of (InclPoset the topology of T); ::_thesis: ( b is_>=_than X implies Un <= b )
assume A2: b is_>=_than X ; ::_thesis: Un <= b
now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_
Z_c=_b
let Z be set ; ::_thesis: ( Z in X implies Z c= b )
assume A3: Z in X ; ::_thesis: Z c= b
then reconsider Z9 = Z as Element of (InclPoset the topology of T) ;
 Z9 <= b by A2, A3, LATTICE3:def_9;
hence  Z c= b by Th3; ::_thesis: verum
end;
then  Un c= b by ZFMISC_1:76;
hence  Un <= b by Th3; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_(InclPoset_the_topology_of_T)_st_b_in_X_holds_
b_<=_Un
let b be Element of (InclPoset the topology of T); ::_thesis: ( b in X implies b <= Un )
assume  b in X ; ::_thesis: b <= Un
then  b c= Un by ZFMISC_1:74;
hence  b <= Un by Th3; ::_thesis: verum
end;
then  Un is_>=_than X by LATTICE3:def_9;
hence  sup X = union X by A1, YELLOW_0:30; ::_thesis: verum
end;

theorem :: YELLOW_1:23
for T being non empty TopSpace holds Bottom (InclPoset the topology of T) = {} by Th13, PRE_TOPC:1;

Lm2:  for T being non empty TopSpace holds InclPoset the topology of T is lower-bounded
proof
let T be non empty TopSpace; ::_thesis: InclPoset the topology of T is lower-bounded
set L = InclPoset the topology of T;
reconsider x = {} as Element of (InclPoset the topology of T) by PRE_TOPC:1;
now__::_thesis:_ex_x_being_Element_of_(InclPoset_the_topology_of_T)_st_x_is_<=_than_the_carrier_of_(InclPoset_the_topology_of_T)
take x = x; ::_thesis: x is_<=_than the carrier of (InclPoset the topology of T)
thus  x is_<=_than the carrier of (InclPoset the topology of T) ::_thesis: verum
proof
let b be Element of (InclPoset the topology of T); :: according to LATTICE3:def_8 ::_thesis: ( not b in the carrier of (InclPoset the topology of T) or x <= b )
assume  b in the carrier of (InclPoset the topology of T) ; ::_thesis: x <= b
 x c= b by XBOOLE_1:2;
hence  x <= b by Th3; ::_thesis: verum
end;
end;
hence  InclPoset the topology of T is lower-bounded by YELLOW_0:def_4; ::_thesis: verum
end;

theorem :: YELLOW_1:24
for T being non empty TopSpace holds Top (InclPoset the topology of T) = the carrier of T
proof
let T be non empty TopSpace; ::_thesis: Top (InclPoset the topology of T) = the carrier of T
set L = InclPoset the topology of T;
set C = the carrier of T;
 the carrier of T = "/\" ({},(InclPoset the topology of T))
proof
reconsider C = the carrier of T as Element of (InclPoset the topology of T) by PRE_TOPC:def_1;
A1: for b being Element of (InclPoset the topology of T) st b is_<=_than {} holds
C >= b
proof
let b be Element of (InclPoset the topology of T); ::_thesis: ( b is_<=_than {} implies C >= b )
assume  b is_<=_than {} ; ::_thesis: C >= b
 b in the topology of T ;
hence  C >= b by Th3; ::_thesis: verum
end;
 C is_<=_than {} by YELLOW_0:6;
hence  the carrier of T = "/\" ({},(InclPoset the topology of T)) by A1, YELLOW_0:31; ::_thesis: verum
end;
hence  Top (InclPoset the topology of T) = the carrier of T by YELLOW_0:def_12; ::_thesis: verum
end;

Lm3:  for T being non empty TopSpace holds InclPoset the topology of T is complete
proof
let T be non empty TopSpace; ::_thesis: InclPoset the topology of T is complete
set A = the topology of T;
reconsider IA = InclPoset the topology of T as lower-bounded Poset by Lm2;
 for X being Subset of IA holds ex_sup_of X, InclPoset the topology of T
proof
let X be Subset of IA; ::_thesis: ex_sup_of X, InclPoset the topology of T
set N = union X;
reconsider X9 = X as Subset-Family of T by XBOOLE_1:1;
 X9 c= the topology of T ;
then reconsider N = union X as Element of (InclPoset the topology of T) by PRE_TOPC:def_1;
A1: for b being Element of (InclPoset the topology of T) st X is_<=_than b holds
N <= b
proof
let b be Element of (InclPoset the topology of T); ::_thesis: ( X is_<=_than b implies N <= b )
assume A2: X is_<=_than b ; ::_thesis: N <= b
now__::_thesis:_for_Z1_being_set_st_Z1_in_X_holds_
Z1_c=_b
let Z1 be set ; ::_thesis: ( Z1 in X implies Z1 c= b )
assume A3: Z1 in X ; ::_thesis: Z1 c= b
then reconsider Z19 = Z1 as Element of (InclPoset the topology of T) ;
 Z19 <= b by A2, A3, LATTICE3:def_9;
hence  Z1 c= b by Th3; ::_thesis: verum
end;
then  union X c= b by ZFMISC_1:76;
hence  N <= b by Th3; ::_thesis: verum
end;
 X is_<=_than N
proof
let b be Element of (InclPoset the topology of T); :: according to LATTICE3:def_9 ::_thesis: ( not b in X or b <= N )
assume  b in X ; ::_thesis: b <= N
then  b c= N by ZFMISC_1:74;
hence  b <= N by Th3; ::_thesis: verum
end;
hence  ex_sup_of X, InclPoset the topology of T by A1, YELLOW_0:15; ::_thesis: verum
end;
hence  InclPoset the topology of T is complete by YELLOW_0:53; ::_thesis: verum
end;

Lm4:  for T being non empty TopSpace holds not InclPoset the topology of T is trivial
proof
let T be non empty TopSpace; ::_thesis: not InclPoset the topology of T is trivial
set L = InclPoset the topology of T;
reconsider E = {} , S = the carrier of T as Element of (InclPoset the topology of T) by PRE_TOPC:1, PRE_TOPC:def_1;
 E <> S ;
hence  not InclPoset the topology of T is trivial by STRUCT_0:def_10; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
cluster InclPoset the topology of T ->  non trivial strict complete ;
coherence
 ( InclPoset the topology of T is complete & not InclPoset the topology of T is trivial ) by Lm3, Lm4;
end;

theorem :: YELLOW_1:25
for T being TopSpace
for F being Subset-Family of T holds
( F is open iff F is Subset of (InclPoset the topology of T) )
proof
let T be TopSpace; ::_thesis: for F being Subset-Family of T holds
( F is open iff F is Subset of (InclPoset the topology of T) )
let F be Subset-Family of T; ::_thesis: ( F is open iff F is Subset of (InclPoset the topology of T) )
hereby  ::_thesis: ( F is Subset of (InclPoset the topology of T) implies F is open )
assume A1: F is open ; ::_thesis: F is Subset of (InclPoset the topology of T)
 F c= the topology of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in F or a in the topology of T )
assume A2: a in F ; ::_thesis: a in the topology of T
then reconsider a9 = a as Subset of T ;
 a9 is open by A1, A2, TOPS_2:def_1;
hence  a in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
hence  F is Subset of (InclPoset the topology of T) ; ::_thesis: verum
end;
assume A3: F is Subset of (InclPoset the topology of T) ; ::_thesis: F is open
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in F or P is open )
assume  P in F ; ::_thesis: P is open
hence  P is open by A3, PRE_TOPC:def_2; ::_thesis: verum
end;

begin


definition
let R be Relation;
attrR is RelStr-yielding  means :Def3: :: YELLOW_1:def 3
 for v being set st v in rng R holds
v is RelStr ;
end;

:: deftheorem Def3 defines RelStr-yielding YELLOW_1:def_3_:_
 for R being Relation holds
( R is RelStr-yielding iff for v being set st v in rng R holds
v is RelStr );

registration
cluster Relation-like Function-like RelStr-yielding  ->  1-sorted-yielding for set ;
coherence
 for b1 being Function st b1 is RelStr-yielding holds
b1 is 1-sorted-yielding
proof
let F be Function; ::_thesis: ( F is RelStr-yielding implies F is 1-sorted-yielding )
assume A1: F is RelStr-yielding ; ::_thesis: F is 1-sorted-yielding
let x be set ; :: according to PRALG_1:def_11 ::_thesis: ( not x in dom F or F . x is 1-sorted )
assume  x in dom F ; ::_thesis: F . x is 1-sorted
then  F . x in rng F by FUNCT_1:def_3;
hence  F . x is 1-sorted by A1, Def3; ::_thesis: verum
end;
end;

registration
let I be set ;
cluster Relation-like I -defined Function-like V34(I) RelStr-yielding for set ;
existence
 ex b1 being ManySortedSet of I st b1 is RelStr-yielding
proof
set R = the RelStr ;
take  I --> the RelStr ; ::_thesis: I --> the RelStr is RelStr-yielding
let v be set ; :: according to YELLOW_1:def_3 ::_thesis: ( v in rng (I --> the RelStr ) implies v is RelStr )
assume A1: v in rng (I --> the RelStr ) ; ::_thesis: v is RelStr
 rng (I --> the RelStr ) c= { the RelStr } by FUNCOP_1:13;
hence  v is RelStr by A1, TARSKI:def_1; ::_thesis: verum
end;
end;

definition
let J be non empty set ;
let A be RelStr-yielding ManySortedSet of J;
let j be Element of J;
:: original: .
redefine funcA . j ->  RelStr ;
coherence
 A . j is RelStr
proof
 dom A = J by PARTFUN1:def_2;
then  A . j in rng A by FUNCT_1:def_3;
hence  A . j is RelStr by Def3; ::_thesis: verum
end;
end;

definition
let I be set ;
let J be RelStr-yielding ManySortedSet of I;
func product J ->  strict RelStr  means :Def4: :: YELLOW_1:def 4
( the carrier of it = product (Carrier J) & ( for x, y being Element of it st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) );
existence
 ex b1 being strict RelStr st
( the carrier of b1 = product (Carrier J) & ( for x, y being Element of b1 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) )
proof
defpred S1[ set , set ] means  ex f, g being Function st
( f = $1 & g = $2 & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) );
consider R being Relation of (product (Carrier J)) such that
A1: for x, y being set holds
( [x,y] in R iff ( x in product (Carrier J) & y in product (Carrier J) & S1[x,y] ) ) from RELSET_1:sch_1();
take RS = RelStr(# (product (Carrier J)),R #); ::_thesis: ( the carrier of RS = product (Carrier J) & ( for x, y being Element of RS st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) )
thus  the carrier of RS = product (Carrier J) ; ::_thesis: for x, y being Element of RS st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) )
let x, y be Element of RS; ::_thesis: ( x in product (Carrier J) implies ( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) )
assume A2: x in product (Carrier J) ; ::_thesis: ( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) )
hereby  ::_thesis: ( ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) implies x <= y )
assume  x <= y ; ::_thesis: ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) )
then  [x,y] in the InternalRel of RS by ORDERS_2:def_5;
hence  ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) by A1; ::_thesis: verum
end;
assume  ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ; ::_thesis: x <= y
then  [x,y] in the InternalRel of RS by A1, A2;
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict RelStr st the carrier of b1 = product (Carrier J) & ( for x, y being Element of b1 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) & the carrier of b2 = product (Carrier J) & ( for x, y being Element of b2 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) holds
b1 = b2
proof
let S1, S2 be strict RelStr ; ::_thesis: ( the carrier of S1 = product (Carrier J) & ( for x, y being Element of S1 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) & the carrier of S2 = product (Carrier J) & ( for x, y being Element of S2 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) implies S1 = S2 )
assume that
A3: the carrier of S1 = product (Carrier J) and
A4: for x, y being Element of S1 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) and
A5: the carrier of S2 = product (Carrier J) and
A6: for x, y being Element of S2 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ; ::_thesis: S1 = S2
 the InternalRel of S1 = the InternalRel of S2
proof
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in the InternalRel of S1 or [a,b] in the InternalRel of S2 ) & ( not [a,b] in the InternalRel of S2 or [a,b] in the InternalRel of S1 ) )
hereby  ::_thesis: ( not [a,b] in the InternalRel of S2 or [a,b] in the InternalRel of S1 )
assume A7: [a,b] in the InternalRel of S1 ; ::_thesis: [a,b] in the InternalRel of S2
then reconsider x = a, y = b as Element of S1 by ZFMISC_1:87;
reconsider x9 = x, y9 = y as Element of S2 by A3, A5;
A8: a in the carrier of S1 by A7, ZFMISC_1:87;
 x <= y by A7, ORDERS_2:def_5;
then  ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) by A3, A4, A8;
then  x9 <= y9 by A3, A6, A8;
hence  [a,b] in the InternalRel of S2 by ORDERS_2:def_5; ::_thesis: verum
end;
assume A9: [a,b] in the InternalRel of S2 ; ::_thesis: [a,b] in the InternalRel of S1
then reconsider x = a, y = b as Element of S2 by ZFMISC_1:87;
reconsider x9 = x, y9 = y as Element of S1 by A3, A5;
A10: a in the carrier of S2 by A9, ZFMISC_1:87;
 x <= y by A9, ORDERS_2:def_5;
then  ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) by A5, A6, A10;
then  x9 <= y9 by A4, A5, A10;
hence  [a,b] in the InternalRel of S1 by ORDERS_2:def_5; ::_thesis: verum
end;
hence  S1 = S2 by A3, A5; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines product YELLOW_1:def_4_:_
 for I being set
for J being RelStr-yielding ManySortedSet of I
for b3 being strict RelStr holds
( b3 = product J iff ( the carrier of b3 = product (Carrier J) & ( for x, y being Element of b3 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) ) );

registration
let X be set ;
let L be RelStr ;
clusterX --> L ->  RelStr-yielding ;
coherence
 X --> L is RelStr-yielding
proof
let v be set ; :: according to YELLOW_1:def_3 ::_thesis: ( v in rng (X --> L) implies v is RelStr )
assume A1: v in rng (X --> L) ; ::_thesis: v is RelStr
 rng (X --> L) c= {L} by FUNCOP_1:13;
hence  v is RelStr by A1, TARSKI:def_1; ::_thesis: verum
end;
end;

definition
let I be set ;
let T be RelStr ;
funcT |^ I ->  strict RelStr  equals :: YELLOW_1:def 5
 product (I --> T);
correctness
coherence
product (I --> T) is strict RelStr ;
;
end;

:: deftheorem  defines |^ YELLOW_1:def_5_:_
 for I being set
for T being RelStr holds T |^ I = product (I --> T);

theorem Th26: :: YELLOW_1:26
for J being RelStr-yielding ManySortedSet of {} holds product J = RelStr(# {{}},(id {{}}) #)
proof
let J be RelStr-yielding ManySortedSet of {} ; ::_thesis: product J = RelStr(# {{}},(id {{}}) #)
set IT = product J;
A1: the carrier of (product J) = product (Carrier J) by Def4
.= {{}} by CARD_3:10, PBOOLE:122 ;
A2: product (Carrier J) = {{}} by CARD_3:10, PBOOLE:122;
 the InternalRel of (product J) = id {{}}
proof
reconsider x = {} , y = {} as Element of (product J) by A1, TARSKI:def_1;
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in the InternalRel of (product J) or [a,b] in id {{}} ) & ( not [a,b] in id {{}} or [a,b] in the InternalRel of (product J) ) )
 x = {} --> {{}} ;
then reconsider f = x, g = y as Function ;
hereby  ::_thesis: ( not [a,b] in id {{}} or [a,b] in the InternalRel of (product J) )
assume A3: [a,b] in the InternalRel of (product J) ; ::_thesis: [a,b] in id {{}}
then A4: b in the carrier of (product J) by ZFMISC_1:87;
A5: a in the carrier of (product J) by A3, ZFMISC_1:87;
then  a = {} by A1, TARSKI:def_1;
then  a = b by A1, A4, TARSKI:def_1;
hence  [a,b] in id {{}} by A1, A5, RELAT_1:def_10; ::_thesis: verum
end;
assume A6: [a,b] in id {{}} ; ::_thesis: [a,b] in the InternalRel of (product J)
then  a in {{}} by RELAT_1:def_10;
then A7: a = {} by TARSKI:def_1;
 for i being set st i in {} holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ;
then A8: x <= y by A1, A2, Def4;
 a = b by A6, RELAT_1:def_10;
hence  [a,b] in the InternalRel of (product J) by A7, A8, ORDERS_2:def_5; ::_thesis: verum
end;
hence  product J = RelStr(# {{}},(id {{}}) #) by A1; ::_thesis: verum
end;

theorem :: YELLOW_1:27
for Y being RelStr holds Y |^ {} = RelStr(# {{}},(id {{}}) #) by Th26;

theorem Th28: :: YELLOW_1:28
for X being set
for Y being RelStr holds Funcs (X, the carrier of Y) = the carrier of (Y |^ X)
proof
let X be set ; ::_thesis: for Y being RelStr holds Funcs (X, the carrier of Y) = the carrier of (Y |^ X)
let Y be RelStr ; ::_thesis: Funcs (X, the carrier of Y) = the carrier of (Y |^ X)
set YY = the carrier of Y;
set f = Carrier (X --> Y);
A1: dom (Carrier (X --> Y)) = X by PARTFUN1:def_2;
A2: for x being set st x in X holds
(Carrier (X --> Y)) . x = the carrier of Y
proof
let x be set ; ::_thesis: ( x in X implies (Carrier (X --> Y)) . x = the carrier of Y )
assume A3: x in X ; ::_thesis: (Carrier (X --> Y)) . x = the carrier of Y
then  ex R being 1-sorted st
( R = (X --> Y) . x & (Carrier (X --> Y)) . x = the carrier of R ) by PRALG_1:def_13;
hence  (Carrier (X --> Y)) . x = the carrier of Y by A3, FUNCOP_1:7; ::_thesis: verum
end;
 Funcs (X, the carrier of Y) = product (Carrier (X --> Y))
proof
thus  Funcs (X, the carrier of Y) c= product (Carrier (X --> Y)) :: according to XBOOLE_0:def_10 ::_thesis: product (Carrier (X --> Y)) c= Funcs (X, the carrier of Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (X, the carrier of Y) or x in product (Carrier (X --> Y)) )
assume  x in Funcs (X, the carrier of Y) ; ::_thesis: x in product (Carrier (X --> Y))
then consider g being Function such that
A4: x = g and
A5: dom g = X and
A6: rng g c= the carrier of Y by FUNCT_2:def_2;
now__::_thesis:_for_y_being_set_st_y_in_dom_(Carrier_(X_-->_Y))_holds_
g_._y_in_(Carrier_(X_-->_Y))_._y
let y be set ; ::_thesis: ( y in dom (Carrier (X --> Y)) implies g . y in (Carrier (X --> Y)) . y )
assume  y in dom (Carrier (X --> Y)) ; ::_thesis: g . y in (Carrier (X --> Y)) . y
then  ( (Carrier (X --> Y)) . y = the carrier of Y & g . y in rng g ) by A2, A5, FUNCT_1:def_3;
hence  g . y in (Carrier (X --> Y)) . y by A6; ::_thesis: verum
end;
hence  x in product (Carrier (X --> Y)) by A1, A4, A5, CARD_3:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (Carrier (X --> Y)) or x in Funcs (X, the carrier of Y) )
assume  x in product (Carrier (X --> Y)) ; ::_thesis: x in Funcs (X, the carrier of Y)
then consider g being Function such that
A7: x = g and
A8: dom g = dom (Carrier (X --> Y)) and
A9: for x being set st x in dom (Carrier (X --> Y)) holds
g . x in (Carrier (X --> Y)) . x by CARD_3:def_5;
 rng g c= the carrier of Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in the carrier of Y )
assume  y in rng g ; ::_thesis: y in the carrier of Y
then consider z being set  such that
A10: z in dom g and
A11: y = g . z by FUNCT_1:def_3;
 (Carrier (X --> Y)) . z = the carrier of Y by A2, A8, A10;
hence  y in the carrier of Y by A8, A9, A10, A11; ::_thesis: verum
end;
hence  x in Funcs (X, the carrier of Y) by A1, A7, A8, FUNCT_2:def_2; ::_thesis: verum
end;
hence  Funcs (X, the carrier of Y) = the carrier of (Y |^ X) by Def4; ::_thesis: verum
end;

registration
let X be set ;
let Y be non empty RelStr ;
clusterY |^ X ->  non empty strict ;
coherence
 not Y |^ X is empty
proof
set f = the Function of X, the carrier of Y;
 the Function of X, the carrier of Y in Funcs (X, the carrier of Y) by FUNCT_2:8;
hence  not Y |^ X is empty by Th28; ::_thesis: verum
end;
end;

Lm5:  for X being set
for Y being non empty RelStr
for x being Element of (Y |^ X) holds
( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y )
proof
let X be set ; ::_thesis: for Y being non empty RelStr
for x being Element of (Y |^ X) holds
( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y )
let Y be non empty RelStr ; ::_thesis: for x being Element of (Y |^ X) holds
( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y )
let x be Element of (Y |^ X); ::_thesis: ( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y )
 x in the carrier of (Y |^ X) ;
then  x in Funcs (X, the carrier of Y) by Th28;
hence  ( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y ) by FUNCT_2:66; ::_thesis: verum
end;

registration
let X be set ;
let Y be non empty reflexive RelStr ;
clusterY |^ X ->  strict reflexive ;
coherence
 Y |^ X is reflexive
proof
percases ( X is empty or not X is empty ) ;
suppose X is empty ; ::_thesis: Y |^ X is reflexive
hence  Y |^ X is reflexive by Th26; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: Y |^ X is reflexive
then reconsider X = X as non empty set ;
 for x being Element of (Y |^ X) holds x <= x
proof
let x be Element of (Y |^ X); ::_thesis: x <= x
reconsider x1 = x as Function of X, the carrier of Y by Lm5;
reconsider x9 = x as Element of (product (X --> Y)) ;
A1: ex f, g being Function st
( f = x9 & g = x9 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take  x1 ; ::_thesis: ex g being Function st
( x1 = x9 & g = x9 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = g . i & xi <= yi ) ) )
take  x1 ; ::_thesis: ( x1 = x9 & x1 = x9 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi ) ) )
thus  ( x1 = x9 & x1 = x9 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi ) )
assume  i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
then reconsider i = i as Element of X ;
take R = (X --> Y) . i; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
reconsider xi = x1 . i, yi = x1 . i as Element of R by FUNCOP_1:7;
take  xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
take  yi ; ::_thesis: ( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
reconsider xi1 = xi, yi1 = xi as Element of Y ;
 xi1 <= yi1 ;
hence  ( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi ) by FUNCOP_1:7; ::_thesis: verum
end;
 x in the carrier of (product (X --> Y)) ;
then  x9 in product (Carrier (X --> Y)) by Def4;
hence  x <= x by A1, Def4; ::_thesis: verum
end;
hence  Y |^ X is reflexive by YELLOW_0:def_1; ::_thesis: verum
end;
end;
end;
end;

registration
let Y be non empty RelStr ;
clusterY |^ {} -> 1 -element strict ;
coherence
 Y |^ {} is 1 -element by Th26;
end;

registration
let Y be non empty reflexive RelStr ;
clusterY |^ {} ->  strict antisymmetric with_suprema with_infima ;
coherence
 ( Y |^ {} is with_infima & Y |^ {} is with_suprema & Y |^ {} is antisymmetric ) ;
end;

registration
let X be set ;
let Y be non empty transitive RelStr ;
clusterY |^ X ->  strict transitive ;
coherence
 Y |^ X is transitive
proof
set IT = Y |^ X;
now__::_thesis:_for_x,_y,_z_being_Element_of_(Y_|^_X)_st_x_<=_y_&_y_<=_z_holds_
x_<=_z
let x, y, z be Element of (Y |^ X); ::_thesis: ( x <= y & y <= z implies x <= z )
reconsider x1 = x, y1 = y, z1 = z as Element of (product (X --> Y)) ;
assume that
A1: x <= y and
A2: y <= z ; ::_thesis: x <= z
 y1 in the carrier of (product (X --> Y)) ;
then  y1 in product (Carrier (X --> Y)) by Def4;
then consider f1, g1 being Function such that
A3: ( f1 = y1 & g1 = z1 ) and
A4: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f1 . i & yi = g1 . i & xi <= yi ) by A2, Def4;
 x1 in the carrier of (product (X --> Y)) ;
then A5: x1 in product (Carrier (X --> Y)) by Def4;
then consider f, g being Function such that
A6: ( f = x1 & g = y1 ) and
A7: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) by A1, Def4;
 ex f2, g2 being Function st
( f2 = x1 & g2 = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) ) )
proof
reconsider f2 = x, g2 = z as Function of X, the carrier of Y by Lm5;
take  f2 ; ::_thesis: ex g2 being Function st
( f2 = x1 & g2 = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) ) )
take  g2 ; ::_thesis: ( f2 = x1 & g2 = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) ) )
thus  ( f2 = x1 & g2 = z1 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) )
assume A8: i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
then reconsider X = X as non empty set ;
reconsider i = i as Element of X by A8;
reconsider R = (X --> Y) . i as RelStr ;
A9: R = Y by FUNCOP_1:7;
then reconsider xi = f2 . i, yi = g2 . i as Element of R by FUNCT_2:5;
take  R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
take  xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
take  yi ; ::_thesis: ( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
 ( ex R1 being RelStr ex xi1, yi1 being Element of R1 st
( R1 = (X --> Y) . i & xi1 = f . i & yi1 = g . i & xi1 <= yi1 ) & ex R2 being RelStr ex xi2, yi2 being Element of R2 st
( R2 = (X --> Y) . i & xi2 = f1 . i & yi2 = g1 . i & xi2 <= yi2 ) ) by A7, A4;
hence  ( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) by A6, A3, A9, YELLOW_0:def_2; ::_thesis: verum
end;
hence  x <= z by A5, Def4; ::_thesis: verum
end;
hence  Y |^ X is transitive by YELLOW_0:def_2; ::_thesis: verum
end;
end;

registration
let X be set ;
let Y be non empty antisymmetric RelStr ;
clusterY |^ X ->  strict antisymmetric ;
coherence
 Y |^ X is antisymmetric
proof
set IT = Y |^ X;
now__::_thesis:_for_x,_y_being_Element_of_(Y_|^_X)_st_x_<=_y_&_y_<=_x_holds_
x_=_y
let x, y be Element of (Y |^ X); ::_thesis: ( x <= y & y <= x implies x = y )
reconsider x19 = x, y19 = y as Function of X, the carrier of Y by Lm5;
reconsider x1 = x, y1 = y as Element of (product (X --> Y)) ;
assume that
A1: x <= y and
A2: y <= x ; ::_thesis: x = y
 y1 in the carrier of (product (X --> Y)) ;
then  y1 in product (Carrier (X --> Y)) by Def4;
then consider f1, g1 being Function such that
A3: ( f1 = y1 & g1 = x1 ) and
A4: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f1 . i & yi = g1 . i & xi <= yi ) by A2, Def4;
 x1 in the carrier of (product (X --> Y)) ;
then  x1 in product (Carrier (X --> Y)) by Def4;
then consider f, g being Function such that
A5: ( f = x1 & g = y1 ) and
A6: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) by A1, Def4;
A7: now__::_thesis:_for_i_being_set_st_i_in_X_holds_
x19_._i_=_y19_._i
let i be set ; ::_thesis: ( i in X implies x19 . i = y19 . i )
assume A8: i in X ; ::_thesis: x19 . i = y19 . i
then consider R2 being RelStr , xi2, yi2 being Element of R2 such that
A9: R2 = (X --> Y) . i and
A10: ( xi2 = f1 . i & yi2 = g1 . i & xi2 <= yi2 ) by A4;
A11: Y = R2 by A8, A9, FUNCOP_1:7;
consider R1 being RelStr , xi1, yi1 being Element of R1 such that
A12: R1 = (X --> Y) . i and
A13: ( xi1 = f . i & yi1 = g . i & xi1 <= yi1 ) by A6, A8;
 Y = R1 by A8, A12, FUNCOP_1:7;
hence  x19 . i = y19 . i by A5, A3, A13, A10, A11, ORDERS_2:2; ::_thesis: verum
end;
 ( dom x19 = X & dom y19 = X ) by FUNCT_2:def_1;
hence  x = y by A7, FUNCT_1:2; ::_thesis: verum
end;
hence  Y |^ X is antisymmetric by YELLOW_0:def_3; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let Y be non empty antisymmetric with_infima RelStr ;
clusterY |^ X ->  strict with_infima ;
coherence
 Y |^ X is with_infima
proof
set IT = Y |^ X;
let x, y be Element of (Y |^ X); :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of (Y |^ X) st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of (Y |^ X) holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
reconsider y9 = y as Function of X, the carrier of Y by Lm5;
reconsider x9 = x as Function of X, the carrier of Y by Lm5;
defpred S1[ set , set ] means  ex xa, ya being Element of Y st
( xa = x9 . X & ya = y9 . X & Y = xa "/\" ya );
A1: for x being set st x in X holds
ex y being set st
( y in the carrier of Y & S1[x,y] )
proof
let a be set ; ::_thesis: ( a in X implies ex y being set st
( y in the carrier of Y & S1[a,y] ) )
assume  a in X ; ::_thesis: ex y being set st
( y in the carrier of Y & S1[a,y] )
then reconsider xa = x9 . a, ya = y9 . a as Element of Y by FUNCT_2:5;
take y = xa "/\" ya; ::_thesis: ( y in the carrier of Y & S1[a,y] )
thus  y in the carrier of Y ; ::_thesis: S1[a,y]
take  xa ; ::_thesis: ex ya being Element of Y st
( xa = x9 . a & ya = y9 . a & y = xa "/\" ya )
take  ya ; ::_thesis: ( xa = x9 . a & ya = y9 . a & y = xa "/\" ya )
thus  ( xa = x9 . a & ya = y9 . a & y = xa "/\" ya ) ; ::_thesis: verum
end;
consider f being Function of X, the carrier of Y such that
A2: for a being set st a in X holds
S1[a,f . a] from FUNCT_2:sch_1(A1);
 f in Funcs (X, the carrier of Y) by FUNCT_2:8;
then reconsider z = f as Element of (Y |^ X) by Th28;
take  z ; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of (Y |^ X) holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )
A3: z <= y
proof
reconsider y1 = y, z1 = z as Element of (product (X --> Y)) ;
A4: ex f, g being Function st
( f = z1 & g = y1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take  f ; ::_thesis: ex g being Function st
( f = z1 & g = y1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
take  y9 ; ::_thesis: ( f = z1 & y9 = y1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi ) ) )
thus  ( f = z1 & y9 = y1 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi ) )
assume  i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider xi = f . i, yi = y9 . i as Element of R by FUNCOP_1:7;
take  R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
take  xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
take  yi ; ::_thesis: ( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
 ( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "/\" ya ) ) by A2, FUNCOP_1:7;
hence  ( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi ) by YELLOW_0:23; ::_thesis: verum
end;
 z1 in the carrier of (product (X --> Y)) ;
then  z1 in product (Carrier (X --> Y)) by Def4;
hence  z <= y by A4, Def4; ::_thesis: verum
end;
A5: for z9 being Element of (Y |^ X) st z9 <= x & z9 <= y holds
z9 <= z
proof
let z9 be Element of (Y |^ X); ::_thesis: ( z9 <= x & z9 <= y implies z9 <= z )
assume that
A6: z9 <= x and
A7: z9 <= y ; ::_thesis: z9 <= z
 z9 <= z
proof
reconsider z2 = z9, z3 = z, z4 = y, z5 = x as Element of (product (X --> Y)) ;
reconsider J = z2, K = z3 as Function of X, the carrier of Y by Lm5;
 z9 in the carrier of (product (X --> Y)) ;
then A8: z2 in product (Carrier (X --> Y)) by Def4;
then consider f1, g1 being Function such that
A9: ( f1 = z2 & g1 = z5 ) and
A10: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f1 . i & yi = g1 . i & xi <= yi ) by A6, Def4;
consider f2, g2 being Function such that
A11: ( f2 = z2 & g2 = z4 ) and
A12: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) by A7, A8, Def4;
 ex f, g being Function st
( f = z2 & g = z3 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take  J ; ::_thesis: ex g being Function st
( J = z2 & g = z3 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = g . i & xi <= yi ) ) )
take  K ; ::_thesis: ( J = z2 & K = z3 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi ) ) )
thus  ( J = z2 & K = z3 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi ) )
assume  i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider xi = J . i, yi = K . i as Element of R by FUNCOP_1:7;
take  R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
take  xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
take  yi ; ::_thesis: ( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
A13: ( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "/\" ya ) ) by A2, FUNCOP_1:7;
 ( ex R1 being RelStr ex xi1, yi1 being Element of R1 st
( R1 = (X --> Y) . i & xi1 = f1 . i & yi1 = g1 . i & xi1 <= yi1 ) & ex R2 being RelStr ex xi2, yi2 being Element of R2 st
( R2 = (X --> Y) . i & xi2 = f2 . i & yi2 = g2 . i & xi2 <= yi2 ) ) by A10, A12;
hence  ( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi ) by A9, A11, A13, YELLOW_0:23; ::_thesis: verum
end;
hence  z9 <= z by A8, Def4; ::_thesis: verum
end;
hence  z9 <= z ; ::_thesis: verum
end;
 z <= x
proof
reconsider x1 = x, z1 = z as Element of (product (X --> Y)) ;
A14: ex f, g being Function st
( f = z1 & g = x1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take  f ; ::_thesis: ex g being Function st
( f = z1 & g = x1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
take  x9 ; ::_thesis: ( f = z1 & x9 = x1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi ) ) )
thus  ( f = z1 & x9 = x1 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi ) )
assume  i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider xi = f . i, yi = x9 . i as Element of R by FUNCOP_1:7;
take  R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
take  xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
take  yi ; ::_thesis: ( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
 ( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "/\" ya ) ) by A2, FUNCOP_1:7;
hence  ( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi ) by YELLOW_0:23; ::_thesis: verum
end;
 z1 in the carrier of (product (X --> Y)) ;
then  z1 in product (Carrier (X --> Y)) by Def4;
hence  z <= x by A14, Def4; ::_thesis: verum
end;
hence  ( z <= x & z <= y & ( for b1 being Element of the carrier of (Y |^ X) holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) ) by A3, A5; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let Y be non empty antisymmetric with_suprema RelStr ;
clusterY |^ X ->  strict with_suprema ;
coherence
 Y |^ X is with_suprema
proof
set IT = Y |^ X;
let x, y be Element of (Y |^ X); :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of (Y |^ X) st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of (Y |^ X) holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
reconsider y9 = y as Function of X, the carrier of Y by Lm5;
reconsider x9 = x as Function of X, the carrier of Y by Lm5;
defpred S1[ set , set ] means  ex xa, ya being Element of Y st
( xa = x9 . X & ya = y9 . X & Y = xa "\/" ya );
A1: for x being set st x in X holds
ex y being set st
( y in the carrier of Y & S1[x,y] )
proof
let a be set ; ::_thesis: ( a in X implies ex y being set st
( y in the carrier of Y & S1[a,y] ) )
assume  a in X ; ::_thesis: ex y being set st
( y in the carrier of Y & S1[a,y] )
then reconsider xa = x9 . a, ya = y9 . a as Element of Y by FUNCT_2:5;
take y = xa "\/" ya; ::_thesis: ( y in the carrier of Y & S1[a,y] )
thus  y in the carrier of Y ; ::_thesis: S1[a,y]
take  xa ; ::_thesis: ex ya being Element of Y st
( xa = x9 . a & ya = y9 . a & y = xa "\/" ya )
take  ya ; ::_thesis: ( xa = x9 . a & ya = y9 . a & y = xa "\/" ya )
thus  ( xa = x9 . a & ya = y9 . a & y = xa "\/" ya ) ; ::_thesis: verum
end;
consider f being Function of X, the carrier of Y such that
A2: for a being set st a in X holds
S1[a,f . a] from FUNCT_2:sch_1(A1);
 f in Funcs (X, the carrier of Y) by FUNCT_2:8;
then reconsider z = f as Element of (Y |^ X) by Th28;
take  z ; ::_thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of (Y |^ X) holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )
A3: y <= z
proof
reconsider y1 = y, z1 = z as Element of (product (X --> Y)) ;
A4: ex f, g being Function st
( f = y1 & g = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take  y9 ; ::_thesis: ex g being Function st
( y9 = y1 & g = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = g . i & xi <= yi ) ) )
take  f ; ::_thesis: ( y9 = y1 & f = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi ) ) )
thus  ( y9 = y1 & f = z1 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi ) )
assume  i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider yi = f . i, xi = y9 . i as Element of R by FUNCOP_1:7;
take  R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
take  xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
take  yi ; ::_thesis: ( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
 ( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "\/" ya ) ) by A2, FUNCOP_1:7;
hence  ( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi ) by YELLOW_0:22; ::_thesis: verum
end;
 y1 in the carrier of (product (X --> Y)) ;
then  y1 in product (Carrier (X --> Y)) by Def4;
hence  y <= z by A4, Def4; ::_thesis: verum
end;
A5: for z9 being Element of (Y |^ X) st z9 >= x & z9 >= y holds
z9 >= z
proof
let z9 be Element of (Y |^ X); ::_thesis: ( z9 >= x & z9 >= y implies z9 >= z )
assume that
A6: z9 >= x and
A7: z9 >= y ; ::_thesis: z9 >= z
 z9 >= z
proof
reconsider z2 = z9, z3 = z, z4 = y, z5 = x as Element of (product (X --> Y)) ;
 z4 in the carrier of (product (X --> Y)) ;
then  z4 in product (Carrier (X --> Y)) by Def4;
then consider f2, g2 being Function such that
A8: ( f2 = z4 & g2 = z2 ) and
A9: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) by A7, Def4;
reconsider K = z3, J = z2 as Function of X, the carrier of Y by Lm5;
 z5 in the carrier of (product (X --> Y)) ;
then  z5 in product (Carrier (X --> Y)) by Def4;
then consider f1, g1 being Function such that
A10: ( f1 = z5 & g1 = z2 ) and
A11: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f1 . i & yi = g1 . i & xi <= yi ) by A6, Def4;
A12: ex f, g being Function st
( f = z3 & g = z2 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take  K ; ::_thesis: ex g being Function st
( K = z3 & g = z2 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = g . i & xi <= yi ) ) )
take  J ; ::_thesis: ( K = z3 & J = z2 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi ) ) )
thus  ( K = z3 & J = z2 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi ) )
assume  i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider yi = J . i, xi = K . i as Element of R by FUNCOP_1:7;
take  R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
take  xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
take  yi ; ::_thesis: ( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
A13: ( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "\/" ya ) ) by A2, FUNCOP_1:7;
 ( ex R1 being RelStr ex xi1, yi1 being Element of R1 st
( R1 = (X --> Y) . i & xi1 = f1 . i & yi1 = g1 . i & xi1 <= yi1 ) & ex R2 being RelStr ex xi2, yi2 being Element of R2 st
( R2 = (X --> Y) . i & xi2 = f2 . i & yi2 = g2 . i & xi2 <= yi2 ) ) by A11, A9;
hence  ( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi ) by A10, A8, A13, YELLOW_0:22; ::_thesis: verum
end;
 z3 in the carrier of (product (X --> Y)) ;
then  z3 in product (Carrier (X --> Y)) by Def4;
hence  z9 >= z by A12, Def4; ::_thesis: verum
end;
hence  z9 >= z ; ::_thesis: verum
end;
 x <= z
proof
reconsider x1 = x, z1 = z as Element of (product (X --> Y)) ;
A14: ex f, g being Function st
( f = x1 & g = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take  x9 ; ::_thesis: ex g being Function st
( x9 = x1 & g = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = g . i & xi <= yi ) ) )
take  f ; ::_thesis: ( x9 = x1 & f = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi ) ) )
thus  ( x9 = x1 & f = z1 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi ) )
assume  i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider yi = f . i, xi = x9 . i as Element of R by FUNCOP_1:7;
take  R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
take  xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
take  yi ; ::_thesis: ( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
 ( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "\/" ya ) ) by A2, FUNCOP_1:7;
hence  ( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi ) by YELLOW_0:22; ::_thesis: verum
end;
 x1 in the carrier of (product (X --> Y)) ;
then  x1 in product (Carrier (X --> Y)) by Def4;
hence  x <= z by A14, Def4; ::_thesis: verum
end;
hence  ( x <= z & y <= z & ( for b1 being Element of the carrier of (Y |^ X) holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) ) by A3, A5; ::_thesis: verum
end;
end;

definition
let S, T be RelStr ;
func MonMaps (S,T) ->  strict full SubRelStr of T |^ the carrier of S means :: YELLOW_1:def 6
 for f being Function of S,T holds
( f in the carrier of it iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) );
existence
 ex b1 being strict full SubRelStr of T |^ the carrier of S st
for f being Function of S,T holds
( f in the carrier of b1 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) )
proof
set X = MonFuncs (S,T);
 MonFuncs (S,T) c= Funcs ( the carrier of S, the carrier of T) by ORDERS_3:11;
then reconsider X = MonFuncs (S,T) as Subset of (T |^ the carrier of S) by Th28;
take SX = subrelstr X; ::_thesis: for f being Function of S,T holds
( f in the carrier of SX iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) )
let f be Function of S,T; ::_thesis: ( f in the carrier of SX iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) )
hereby  ::_thesis: ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone implies f in the carrier of SX )
assume  f in the carrier of SX ; ::_thesis: ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone )
then  f in X by YELLOW_0:def_15;
then  ex f9 being Function of S,T st
( f9 = f & f9 in Funcs ( the carrier of S, the carrier of T) & f9 is monotone ) by ORDERS_3:def_6;
hence  ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ; ::_thesis: verum
end;
assume  ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ; ::_thesis: f in the carrier of SX
then  f in X by ORDERS_3:def_6;
hence  f in the carrier of SX by YELLOW_0:def_15; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict full SubRelStr of T |^ the carrier of S st ( for f being Function of S,T holds
( f in the carrier of b1 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) ) & ( for f being Function of S,T holds
( f in the carrier of b2 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) ) holds
b1 = b2
proof
let A1, A2 be strict full SubRelStr of T |^ the carrier of S; ::_thesis: ( ( for f being Function of S,T holds
( f in the carrier of A1 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) ) & ( for f being Function of S,T holds
( f in the carrier of A2 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) ) implies A1 = A2 )
assume that
A1: for f being Function of S,T holds
( f in the carrier of A1 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) and
A2: for f being Function of S,T holds
( f in the carrier of A2 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) ; ::_thesis: A1 = A2
 the carrier of A2 c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13;
then A3: the carrier of A2 c= Funcs ( the carrier of S, the carrier of T) by Th28;
A4: the carrier of A2 c= the carrier of A1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of A2 or a in the carrier of A1 )
assume A5: a in the carrier of A2 ; ::_thesis: a in the carrier of A1
then reconsider f = a as Function of S,T by A3, FUNCT_2:66;
 f is monotone by A2, A5;
hence  a in the carrier of A1 by A1, A3, A5; ::_thesis: verum
end;
 the carrier of A1 c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13;
then A6: the carrier of A1 c= Funcs ( the carrier of S, the carrier of T) by Th28;
 the carrier of A1 c= the carrier of A2
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of A1 or a in the carrier of A2 )
assume A7: a in the carrier of A1 ; ::_thesis: a in the carrier of A2
then reconsider f = a as Function of S,T by A6, FUNCT_2:66;
 f is monotone by A1, A7;
hence  a in the carrier of A2 by A2, A6, A7; ::_thesis: verum
end;
then  the carrier of A1 = the carrier of A2 by A4, XBOOLE_0:def_10;
hence  A1 = A2 by YELLOW_0:57; ::_thesis: verum
end;
end;

:: deftheorem  defines MonMaps YELLOW_1:def_6_:_
 for S, T being RelStr
for b3 being strict full SubRelStr of T |^ the carrier of S holds
( b3 = MonMaps (S,T) iff for f being Function of S,T holds
( f in the carrier of b3 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) );