:: 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 ) ) );