:: WAYBEL_0 semantic presentation begin definition let L be RelStr ; let X be Subset of L; attrX is directed means :Def1: :: WAYBEL_0:def 1 for x, y being Element of L st x in X & y in X holds ex z being Element of L st ( z in X & x <= z & y <= z ); attrX is filtered means :Def2: :: WAYBEL_0:def 2 for x, y being Element of L st x in X & y in X holds ex z being Element of L st ( z in X & z <= x & z <= y ); end; :: deftheorem Def1 defines directed WAYBEL_0:def_1_:_ for L being RelStr for X being Subset of L holds ( X is directed iff for x, y being Element of L st x in X & y in X holds ex z being Element of L st ( z in X & x <= z & y <= z ) ); :: deftheorem Def2 defines filtered WAYBEL_0:def_2_:_ for L being RelStr for X being Subset of L holds ( X is filtered iff for x, y being Element of L st x in X & y in X holds ex z being Element of L st ( z in X & z <= x & z <= y ) ); theorem Th1: :: WAYBEL_0:1 for L being non empty transitive RelStr for X being Subset of L holds ( ( not X is empty & X is directed ) iff for Y being finite Subset of X ex x being Element of L st ( x in X & x is_>=_than Y ) ) proof let L be non empty transitive RelStr ; ::_thesis: for X being Subset of L holds ( ( not X is empty & X is directed ) iff for Y being finite Subset of X ex x being Element of L st ( x in X & x is_>=_than Y ) ) let X be Subset of L; ::_thesis: ( ( not X is empty & X is directed ) iff for Y being finite Subset of X ex x being Element of L st ( x in X & x is_>=_than Y ) ) hereby ::_thesis: ( ( for Y being finite Subset of X ex x being Element of L st ( x in X & x is_>=_than Y ) ) implies ( not X is empty & X is directed ) ) assume not X is empty ; ::_thesis: ( X is directed implies for Y being finite Subset of X holds S1[Y] ) then reconsider X9 = X as non empty set ; assume A1: X is directed ; ::_thesis: for Y being finite Subset of X holds S1[Y] let Y be finite Subset of X; ::_thesis: S1[Y] defpred S1[ set ] means ex x being Element of L st ( x in X & x is_>=_than $1 ); A2: Y is finite ; set x = the Element of X9; the Element of X9 in X ; then reconsider x = the Element of X9 as Element of L ; x is_>=_than {} by YELLOW_0:6; then A3: S1[ {} ] ; A4: now__::_thesis:_for_x,_B_being_set_st_x_in_Y_&_B_c=_Y_&_S1[B]_holds_ S1[B_\/_{x}] let x, B be set ; ::_thesis: ( x in Y & B c= Y & S1[B] implies S1[B \/ {x}] ) assume that A5: x in Y and B c= Y ; ::_thesis: ( S1[B] implies S1[B \/ {x}] ) assume S1[B] ; ::_thesis: S1[B \/ {x}] then consider y being Element of L such that A6: y in X and A7: y is_>=_than B ; x in X by A5; then reconsider x9 = x as Element of L ; consider z being Element of L such that A8: z in X and A9: x9 <= z and A10: y <= z by A1, A5, A6, Def1; thus S1[B \/ {x}] ::_thesis: verum proof take z ; ::_thesis: ( z in X & z is_>=_than B \/ {x} ) thus z in X by A8; ::_thesis: z is_>=_than B \/ {x} let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in B \/ {x} or a <= z ) reconsider a9 = a as Element of L ; assume a in B \/ {x} ; ::_thesis: a <= z then ( a9 in B or a9 in {x} ) by XBOOLE_0:def_3; then ( y >= a9 or a9 = x ) by A7, LATTICE3:def_9, TARSKI:def_1; hence a <= z by A9, A10, ORDERS_2:3; ::_thesis: verum end; end; thus S1[Y] from FINSET_1:sch_2(A2, A3, A4); ::_thesis: verum end; assume A11: for Y being finite Subset of X ex x being Element of L st ( x in X & x is_>=_than Y ) ; ::_thesis: ( not X is empty & X is directed ) {} c= X by XBOOLE_1:2; then ex x being Element of L st ( x in X & x is_>=_than {} ) by A11; hence not X is empty ; ::_thesis: X is directed let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in X & y in X implies ex z being Element of L st ( z in X & x <= z & y <= z ) ) assume that A12: x in X and A13: y in X ; ::_thesis: ex z being Element of L st ( z in X & x <= z & y <= z ) {x,y} c= X by A12, A13, ZFMISC_1:32; then consider z being Element of L such that A14: z in X and A15: z is_>=_than {x,y} by A11; take z ; ::_thesis: ( z in X & x <= z & y <= z ) A16: x in {x,y} by TARSKI:def_2; y in {x,y} by TARSKI:def_2; hence ( z in X & x <= z & y <= z ) by A14, A15, A16, LATTICE3:def_9; ::_thesis: verum end; theorem Th2: :: WAYBEL_0:2 for L being non empty transitive RelStr for X being Subset of L holds ( ( not X is empty & X is filtered ) iff for Y being finite Subset of X ex x being Element of L st ( x in X & x is_<=_than Y ) ) proof let L be non empty transitive RelStr ; ::_thesis: for X being Subset of L holds ( ( not X is empty & X is filtered ) iff for Y being finite Subset of X ex x being Element of L st ( x in X & x is_<=_than Y ) ) let X be Subset of L; ::_thesis: ( ( not X is empty & X is filtered ) iff for Y being finite Subset of X ex x being Element of L st ( x in X & x is_<=_than Y ) ) hereby ::_thesis: ( ( for Y being finite Subset of X ex x being Element of L st ( x in X & x is_<=_than Y ) ) implies ( not X is empty & X is filtered ) ) assume not X is empty ; ::_thesis: ( X is filtered implies for Y being finite Subset of X holds S1[Y] ) then reconsider X9 = X as non empty set ; assume A1: X is filtered ; ::_thesis: for Y being finite Subset of X holds S1[Y] let Y be finite Subset of X; ::_thesis: S1[Y] defpred S1[ set ] means ex x being Element of L st ( x in X & x is_<=_than $1 ); A2: Y is finite ; set x = the Element of X9; the Element of X9 in X ; then reconsider x = the Element of X9 as Element of L ; x is_<=_than {} by YELLOW_0:6; then A3: S1[ {} ] ; A4: now__::_thesis:_for_x,_B_being_set_st_x_in_Y_&_B_c=_Y_&_S1[B]_holds_ S1[B_\/_{x}] let x, B be set ; ::_thesis: ( x in Y & B c= Y & S1[B] implies S1[B \/ {x}] ) assume that A5: x in Y and B c= Y ; ::_thesis: ( S1[B] implies S1[B \/ {x}] ) assume S1[B] ; ::_thesis: S1[B \/ {x}] then consider y being Element of L such that A6: y in X and A7: y is_<=_than B ; x in X by A5; then reconsider x9 = x as Element of L ; consider z being Element of L such that A8: z in X and A9: x9 >= z and A10: y >= z by A1, A5, A6, Def2; thus S1[B \/ {x}] ::_thesis: verum proof take z ; ::_thesis: ( z in X & z is_<=_than B \/ {x} ) thus z in X by A8; ::_thesis: z is_<=_than B \/ {x} let a be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not a in B \/ {x} or z <= a ) reconsider a9 = a as Element of L ; assume a in B \/ {x} ; ::_thesis: z <= a then ( a9 in B or a9 in {x} ) by XBOOLE_0:def_3; then ( y <= a9 or a9 = x ) by A7, LATTICE3:def_8, TARSKI:def_1; hence z <= a by A9, A10, ORDERS_2:3; ::_thesis: verum end; end; thus S1[Y] from FINSET_1:sch_2(A2, A3, A4); ::_thesis: verum end; assume A11: for Y being finite Subset of X ex x being Element of L st ( x in X & x is_<=_than Y ) ; ::_thesis: ( not X is empty & X is filtered ) {} c= X by XBOOLE_1:2; then ex x being Element of L st ( x in X & x is_<=_than {} ) by A11; hence not X is empty ; ::_thesis: X is filtered let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in X & y in X implies ex z being Element of L st ( z in X & z <= x & z <= y ) ) assume that A12: x in X and A13: y in X ; ::_thesis: ex z being Element of L st ( z in X & z <= x & z <= y ) {x,y} c= X by A12, A13, ZFMISC_1:32; then consider z being Element of L such that A14: z in X and A15: z is_<=_than {x,y} by A11; take z ; ::_thesis: ( z in X & z <= x & z <= y ) A16: x in {x,y} by TARSKI:def_2; y in {x,y} by TARSKI:def_2; hence ( z in X & z <= x & z <= y ) by A14, A15, A16, LATTICE3:def_8; ::_thesis: verum end; registration let L be RelStr ; cluster empty -> directed filtered for Element of K10( the carrier of L); coherence for b1 being Subset of L st b1 is empty holds ( b1 is directed & b1 is filtered ) proof let S be Subset of L; ::_thesis: ( S is empty implies ( S is directed & S is filtered ) ) assume S is empty ; ::_thesis: ( S is directed & S is filtered ) then A1: S = {} L ; thus S is directed ::_thesis: S is filtered proof let x be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: for y being Element of L st x in S & y in S holds ex z being Element of L st ( z in S & x <= z & y <= z ) thus for y being Element of L st x in S & y in S holds ex z being Element of L st ( z in S & x <= z & y <= z ) by A1; ::_thesis: verum end; let x be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: for y being Element of L st x in S & y in S holds ex z being Element of L st ( z in S & z <= x & z <= y ) thus for y being Element of L st x in S & y in S holds ex z being Element of L st ( z in S & z <= x & z <= y ) by A1; ::_thesis: verum end; end; registration let L be RelStr ; cluster directed filtered for Element of K10( the carrier of L); existence ex b1 being Subset of L st ( b1 is directed & b1 is filtered ) proof take {} L ; ::_thesis: ( {} L is directed & {} L is filtered ) thus ( {} L is directed & {} L is filtered ) ; ::_thesis: verum end; end; theorem Th3: :: WAYBEL_0:3 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for X1 being Subset of L1 for X2 being Subset of L2 st X1 = X2 & X1 is directed holds X2 is directed proof let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X1 being Subset of L1 for X2 being Subset of L2 st X1 = X2 & X1 is directed holds X2 is directed ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X1 being Subset of L1 for X2 being Subset of L2 st X1 = X2 & X1 is directed holds X2 is directed let X1 be Subset of L1; ::_thesis: for X2 being Subset of L2 st X1 = X2 & X1 is directed holds X2 is directed let X2 be Subset of L2; ::_thesis: ( X1 = X2 & X1 is directed implies X2 is directed ) assume A2: X1 = X2 ; ::_thesis: ( not X1 is directed or X2 is directed ) assume A3: for x, y being Element of L1 st x in X1 & y in X1 holds ex z being Element of L1 st ( z in X1 & x <= z & y <= z ) ; :: according to WAYBEL_0:def_1 ::_thesis: X2 is directed let x, y be Element of L2; :: according to WAYBEL_0:def_1 ::_thesis: ( x in X2 & y in X2 implies ex z being Element of L2 st ( z in X2 & x <= z & y <= z ) ) reconsider x9 = x, y9 = y as Element of L1 by A1; assume that A4: x in X2 and A5: y in X2 ; ::_thesis: ex z being Element of L2 st ( z in X2 & x <= z & y <= z ) consider z9 being Element of L1 such that A6: z9 in X1 and A7: x9 <= z9 and A8: y9 <= z9 by A2, A3, A4, A5; reconsider z = z9 as Element of L2 by A1; take z ; ::_thesis: ( z in X2 & x <= z & y <= z ) thus ( z in X2 & x <= z & y <= z ) by A1, A2, A6, A7, A8, YELLOW_0:1; ::_thesis: verum end; theorem :: WAYBEL_0:4 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for X1 being Subset of L1 for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds X2 is filtered proof let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X1 being Subset of L1 for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds X2 is filtered ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X1 being Subset of L1 for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds X2 is filtered let X1 be Subset of L1; ::_thesis: for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds X2 is filtered let X2 be Subset of L2; ::_thesis: ( X1 = X2 & X1 is filtered implies X2 is filtered ) assume A2: X1 = X2 ; ::_thesis: ( not X1 is filtered or X2 is filtered ) assume A3: for x, y being Element of L1 st x in X1 & y in X1 holds ex z being Element of L1 st ( z in X1 & x >= z & y >= z ) ; :: according to WAYBEL_0:def_2 ::_thesis: X2 is filtered let x, y be Element of L2; :: according to WAYBEL_0:def_2 ::_thesis: ( x in X2 & y in X2 implies ex z being Element of L2 st ( z in X2 & z <= x & z <= y ) ) reconsider x9 = x, y9 = y as Element of L1 by A1; assume that A4: x in X2 and A5: y in X2 ; ::_thesis: ex z being Element of L2 st ( z in X2 & z <= x & z <= y ) consider z9 being Element of L1 such that A6: z9 in X1 and A7: x9 >= z9 and A8: y9 >= z9 by A2, A3, A4, A5; reconsider z = z9 as Element of L2 by A1; take z ; ::_thesis: ( z in X2 & z <= x & z <= y ) thus ( z in X2 & z <= x & z <= y ) by A1, A2, A6, A7, A8, YELLOW_0:1; ::_thesis: verum end; theorem Th5: :: WAYBEL_0:5 for L being non empty reflexive RelStr for x being Element of L holds ( {x} is directed & {x} is filtered ) proof let L be non empty reflexive RelStr ; ::_thesis: for x being Element of L holds ( {x} is directed & {x} is filtered ) let x be Element of L; ::_thesis: ( {x} is directed & {x} is filtered ) set X = {x}; hereby :: according to WAYBEL_0:def_1 ::_thesis: {x} is filtered let z, y be Element of L; ::_thesis: ( z in {x} & y in {x} implies ex x being Element of L st ( x in {x} & z <= x & y <= x ) ) assume that A1: z in {x} and A2: y in {x} ; ::_thesis: ex x being Element of L st ( x in {x} & z <= x & y <= x ) take x = x; ::_thesis: ( x in {x} & z <= x & y <= x ) thus ( x in {x} & z <= x & y <= x ) by A1, A2, TARSKI:def_1; ::_thesis: verum end; hereby :: according to WAYBEL_0:def_2 ::_thesis: verum let z, y be Element of L; ::_thesis: ( z in {x} & y in {x} implies ex x being Element of L st ( x in {x} & x <= z & x <= y ) ) assume that A3: z in {x} and A4: y in {x} ; ::_thesis: ex x being Element of L st ( x in {x} & x <= z & x <= y ) take x = x; ::_thesis: ( x in {x} & x <= z & x <= y ) thus ( x in {x} & x <= z & x <= y ) by A3, A4, TARSKI:def_1; ::_thesis: verum end; end; registration let L be non empty reflexive RelStr ; cluster non empty finite directed filtered for Element of K10( the carrier of L); existence ex b1 being Subset of L st ( b1 is directed & b1 is filtered & not b1 is empty & b1 is finite ) proof set x = the Element of L; take { the Element of L} ; ::_thesis: ( { the Element of L} is directed & { the Element of L} is filtered & not { the Element of L} is empty & { the Element of L} is finite ) thus ( { the Element of L} is directed & { the Element of L} is filtered & not { the Element of L} is empty & { the Element of L} is finite ) by Th5; ::_thesis: verum end; end; registration let L be with_suprema RelStr ; cluster [#] L -> directed ; coherence [#] L is directed proof set X = [#] L; let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st ( z in [#] L & x <= z & y <= z ) ) assume that x in [#] L and y in [#] L ; ::_thesis: ex z being Element of L st ( z in [#] L & x <= z & y <= z ) ex z being Element of L st ( x <= z & y <= z & ( for z9 being Element of L st x <= z9 & y <= z9 holds z <= z9 ) ) by LATTICE3:def_10; hence ex z being Element of L st ( z in [#] L & x <= z & y <= z ) ; ::_thesis: verum end; end; registration let L be non empty upper-bounded RelStr ; cluster [#] L -> directed ; coherence [#] L is directed proof set X = [#] L; let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st ( z in [#] L & x <= z & y <= z ) ) assume that x in [#] L and y in [#] L ; ::_thesis: ex z being Element of L st ( z in [#] L & x <= z & y <= z ) consider z being Element of L such that A1: z is_>=_than [#] L by YELLOW_0:def_5; take z ; ::_thesis: ( z in [#] L & x <= z & y <= z ) thus ( z in [#] L & x <= z & y <= z ) by A1, LATTICE3:def_9; ::_thesis: verum end; end; registration let L be with_infima RelStr ; cluster [#] L -> filtered ; coherence [#] L is filtered proof set X = [#] L; let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st ( z in [#] L & z <= x & z <= y ) ) assume that x in [#] L and y in [#] L ; ::_thesis: ex z being Element of L st ( z in [#] L & z <= x & z <= y ) ex z being Element of L st ( z <= x & z <= y & ( for z9 being Element of L st z9 <= x & z9 <= y holds z9 <= z ) ) by LATTICE3:def_11; hence ex z being Element of L st ( z in [#] L & z <= x & z <= y ) ; ::_thesis: verum end; end; registration let L be non empty lower-bounded RelStr ; cluster [#] L -> filtered ; coherence [#] L is filtered proof set X = [#] L; let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st ( z in [#] L & z <= x & z <= y ) ) assume that x in [#] L and y in [#] L ; ::_thesis: ex z being Element of L st ( z in [#] L & z <= x & z <= y ) consider z being Element of L such that A1: z is_<=_than [#] L by YELLOW_0:def_4; take z ; ::_thesis: ( z in [#] L & z <= x & z <= y ) thus ( z in [#] L & z <= x & z <= y ) by A1, LATTICE3:def_8; ::_thesis: verum end; end; definition let L be non empty RelStr ; let S be SubRelStr of L; attrS is filtered-infs-inheriting means :Def3: :: WAYBEL_0:def 3 for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds "/\" (X,L) in the carrier of S; attrS is directed-sups-inheriting means :Def4: :: WAYBEL_0:def 4 for X being directed Subset of S st X <> {} & ex_sup_of X,L holds "\/" (X,L) in the carrier of S; end; :: deftheorem Def3 defines filtered-infs-inheriting WAYBEL_0:def_3_:_ for L being non empty RelStr for S being SubRelStr of L holds ( S is filtered-infs-inheriting iff for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds "/\" (X,L) in the carrier of S ); :: deftheorem Def4 defines directed-sups-inheriting WAYBEL_0:def_4_:_ for L being non empty RelStr for S being SubRelStr of L holds ( S is directed-sups-inheriting iff for X being directed Subset of S st X <> {} & ex_sup_of X,L holds "\/" (X,L) in the carrier of S ); registration let L be non empty RelStr ; cluster infs-inheriting -> filtered-infs-inheriting for SubRelStr of L; coherence for b1 being SubRelStr of L st b1 is infs-inheriting holds b1 is filtered-infs-inheriting proof let S be SubRelStr of L; ::_thesis: ( S is infs-inheriting implies S is filtered-infs-inheriting ) assume A1: for X being Subset of S st ex_inf_of X,L holds "/\" (X,L) in the carrier of S ; :: according to YELLOW_0:def_18 ::_thesis: S is filtered-infs-inheriting let X be filtered Subset of S; :: according to WAYBEL_0:def_3 ::_thesis: ( X <> {} & ex_inf_of X,L implies "/\" (X,L) in the carrier of S ) thus ( X <> {} & ex_inf_of X,L implies "/\" (X,L) in the carrier of S ) by A1; ::_thesis: verum end; cluster sups-inheriting -> directed-sups-inheriting for SubRelStr of L; coherence for b1 being SubRelStr of L st b1 is sups-inheriting holds b1 is directed-sups-inheriting proof let S be SubRelStr of L; ::_thesis: ( S is sups-inheriting implies S is directed-sups-inheriting ) assume A2: for X being Subset of S st ex_sup_of X,L holds "\/" (X,L) in the carrier of S ; :: according to YELLOW_0:def_19 ::_thesis: S is directed-sups-inheriting let X be directed Subset of S; :: according to WAYBEL_0:def_4 ::_thesis: ( X <> {} & ex_sup_of X,L implies "\/" (X,L) in the carrier of S ) thus ( X <> {} & ex_sup_of X,L implies "\/" (X,L) in the carrier of S ) by A2; ::_thesis: verum end; end; registration let L be non empty RelStr ; cluster non empty strict full infs-inheriting sups-inheriting for SubRelStr of L; existence ex b1 being SubRelStr of L st ( b1 is infs-inheriting & b1 is sups-inheriting & not b1 is empty & b1 is full & b1 is strict ) proof set S = the non empty strict full infs-inheriting sups-inheriting SubRelStr of L; take the non empty strict full infs-inheriting sups-inheriting SubRelStr of L ; ::_thesis: ( the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is infs-inheriting & the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is sups-inheriting & not the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is empty & the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is full & the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is strict ) thus ( the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is infs-inheriting & the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is sups-inheriting & not the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is empty & the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is full & the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is strict ) ; ::_thesis: verum end; end; theorem :: WAYBEL_0:6 for L being non empty transitive RelStr for S being non empty full filtered-infs-inheriting SubRelStr of L for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) proof let L be non empty transitive RelStr ; ::_thesis: for S being non empty full filtered-infs-inheriting SubRelStr of L for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) let S be non empty full filtered-infs-inheriting SubRelStr of L; ::_thesis: for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) let X be filtered Subset of S; ::_thesis: ( X <> {} & ex_inf_of X,L implies ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) ) assume that A1: X <> {} and A2: ex_inf_of X,L ; ::_thesis: ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) "/\" (X,L) in the carrier of S by A1, A2, Def3; hence ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) by A2, YELLOW_0:63; ::_thesis: verum end; theorem :: WAYBEL_0:7 for L being non empty transitive RelStr for S being non empty full directed-sups-inheriting SubRelStr of L for X being directed Subset of S st X <> {} & ex_sup_of X,L holds ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) proof let L be non empty transitive RelStr ; ::_thesis: for S being non empty full directed-sups-inheriting SubRelStr of L for X being directed Subset of S st X <> {} & ex_sup_of X,L holds ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) let S be non empty full directed-sups-inheriting SubRelStr of L; ::_thesis: for X being directed Subset of S st X <> {} & ex_sup_of X,L holds ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) let X be directed Subset of S; ::_thesis: ( X <> {} & ex_sup_of X,L implies ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) ) assume that A1: X <> {} and A2: ex_sup_of X,L ; ::_thesis: ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) "\/" (X,L) in the carrier of S by A1, A2, Def4; hence ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) by A2, YELLOW_0:64; ::_thesis: verum end; begin definition let L1, L2 be RelStr ; let f be Function of L1,L2; attrf is antitone means :: WAYBEL_0:def 5 for x, y being Element of L1 st x <= y holds for a, b being Element of L2 st a = f . x & b = f . y holds a >= b; end; :: deftheorem defines antitone WAYBEL_0:def_5_:_ for L1, L2 being RelStr for f being Function of L1,L2 holds ( f is antitone iff for x, y being Element of L1 st x <= y holds for a, b being Element of L2 st a = f . x & b = f . y holds a >= b ); definition let L be 1-sorted ; attrc2 is strict ; struct NetStr over L -> RelStr ; aggrNetStr(# carrier, InternalRel, mapping #) -> NetStr over L; sel mapping c2 -> Function of the carrier of c2, the carrier of L; end; registration let L be 1-sorted ; let X be non empty set ; let O be Relation of X; let F be Function of X, the carrier of L; cluster NetStr(# X,O,F #) -> non empty ; coherence not NetStr(# X,O,F #) is empty ; end; definition let N be RelStr ; attrN is directed means :Def6: :: WAYBEL_0:def 6 [#] N is directed ; end; :: deftheorem Def6 defines directed WAYBEL_0:def_6_:_ for N being RelStr holds ( N is directed iff [#] N is directed ); registration let L be 1-sorted ; cluster non empty reflexive transitive antisymmetric strict directed for NetStr over L; existence ex b1 being strict NetStr over L st ( not b1 is empty & b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is directed ) proof set X = the with_suprema Poset; set M = the Function of the carrier of the with_suprema Poset, the carrier of L; take N = NetStr(# the carrier of the with_suprema Poset, the InternalRel of the with_suprema Poset, the Function of the carrier of the with_suprema Poset, the carrier of L #); ::_thesis: ( not N is empty & N is reflexive & N is transitive & N is antisymmetric & N is directed ) thus not N is empty ; ::_thesis: ( N is reflexive & N is transitive & N is antisymmetric & N is directed ) A1: the InternalRel of N is_reflexive_in the carrier of N by ORDERS_2:def_2; A2: the InternalRel of N is_transitive_in the carrier of N by ORDERS_2:def_3; the InternalRel of N is_antisymmetric_in the carrier of N by ORDERS_2:def_4; hence ( N is reflexive & N is transitive & N is antisymmetric ) by A1, A2, ORDERS_2:def_2, ORDERS_2:def_3, ORDERS_2:def_4; ::_thesis: N is directed A3: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of the with_suprema Poset, the InternalRel of the with_suprema Poset #) ; [#] the with_suprema Poset = [#] N ; hence [#] N is directed by A3, Th3; :: according to WAYBEL_0:def_6 ::_thesis: verum end; end; definition let L be 1-sorted ; mode prenet of L is non empty directed NetStr over L; end; definition let L be 1-sorted ; mode net of L is transitive prenet of L; end; definition let L be non empty 1-sorted ; let N be non empty NetStr over L; func netmap (N,L) -> Function of N,L equals :: WAYBEL_0:def 7 the mapping of N; coherence the mapping of N is Function of N,L ; let i be Element of N; funcN . i -> Element of L equals :: WAYBEL_0:def 8 the mapping of N . i; correctness coherence the mapping of N . i is Element of L; ; end; :: deftheorem defines netmap WAYBEL_0:def_7_:_ for L being non empty 1-sorted for N being non empty NetStr over L holds netmap (N,L) = the mapping of N; :: deftheorem defines . WAYBEL_0:def_8_:_ for L being non empty 1-sorted for N being non empty NetStr over L for i being Element of N holds N . i = the mapping of N . i; definition let L be non empty RelStr ; let N be non empty NetStr over L; attrN is monotone means :: WAYBEL_0:def 9 netmap (N,L) is monotone ; attrN is antitone means :: WAYBEL_0:def 10 netmap (N,L) is antitone ; end; :: deftheorem defines monotone WAYBEL_0:def_9_:_ for L being non empty RelStr for N being non empty NetStr over L holds ( N is monotone iff netmap (N,L) is monotone ); :: deftheorem defines antitone WAYBEL_0:def_10_:_ for L being non empty RelStr for N being non empty NetStr over L holds ( N is antitone iff netmap (N,L) is antitone ); definition let L be non empty 1-sorted ; let N be non empty NetStr over L; let X be set ; predN is_eventually_in X means :Def11: :: WAYBEL_0:def 11 ex i being Element of N st for j being Element of N st i <= j holds N . j in X; predN is_often_in X means :: WAYBEL_0:def 12 for i being Element of N ex j being Element of N st ( i <= j & N . j in X ); end; :: deftheorem Def11 defines is_eventually_in WAYBEL_0:def_11_:_ for L being non empty 1-sorted for N being non empty NetStr over L for X being set holds ( N is_eventually_in X iff ex i being Element of N st for j being Element of N st i <= j holds N . j in X ); :: deftheorem defines is_often_in WAYBEL_0:def_12_:_ for L being non empty 1-sorted for N being non empty NetStr over L for X being set holds ( N is_often_in X iff for i being Element of N ex j being Element of N st ( i <= j & N . j in X ) ); theorem :: WAYBEL_0:8 for L being non empty 1-sorted for N being non empty NetStr over L for X, Y being set st X c= Y holds ( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) ) proof let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L for X, Y being set st X c= Y holds ( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) ) let N be non empty NetStr over L; ::_thesis: for X, Y being set st X c= Y holds ( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) ) let X, Y be set ; ::_thesis: ( X c= Y implies ( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) ) ) assume A1: X c= Y ; ::_thesis: ( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) ) hereby ::_thesis: ( N is_often_in X implies N is_often_in Y ) assume N is_eventually_in X ; ::_thesis: N is_eventually_in Y then consider i being Element of N such that A2: for j being Element of N st i <= j holds N . j in X by Def11; thus N is_eventually_in Y ::_thesis: verum proof take i ; :: according to WAYBEL_0:def_11 ::_thesis: for j being Element of N st i <= j holds N . j in Y let j be Element of N; ::_thesis: ( i <= j implies N . j in Y ) assume i <= j ; ::_thesis: N . j in Y then N . j in X by A2; hence N . j in Y by A1; ::_thesis: verum end; end; assume A3: for i being Element of N ex j being Element of N st ( i <= j & N . j in X ) ; :: according to WAYBEL_0:def_12 ::_thesis: N is_often_in Y let i be Element of N; :: according to WAYBEL_0:def_12 ::_thesis: ex j being Element of N st ( i <= j & N . j in Y ) consider j being Element of N such that A4: i <= j and A5: N . j in X by A3; take j ; ::_thesis: ( i <= j & N . j in Y ) thus ( i <= j & N . j in Y ) by A1, A4, A5; ::_thesis: verum end; theorem :: WAYBEL_0:9 for L being non empty 1-sorted for N being non empty NetStr over L for X being set holds ( N is_eventually_in X iff not N is_often_in the carrier of L \ X ) proof let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L for X being set holds ( N is_eventually_in X iff not N is_often_in the carrier of L \ X ) let N be non empty NetStr over L; ::_thesis: for X being set holds ( N is_eventually_in X iff not N is_often_in the carrier of L \ X ) let X be set ; ::_thesis: ( N is_eventually_in X iff not N is_often_in the carrier of L \ X ) set Y = the carrier of L \ X; thus ( N is_eventually_in X implies not N is_often_in the carrier of L \ X ) ::_thesis: ( not N is_often_in the carrier of L \ X implies N is_eventually_in X ) proof given i being Element of N such that A1: for j being Element of N st i <= j holds N . j in X ; :: according to WAYBEL_0:def_11 ::_thesis: not N is_often_in the carrier of L \ X take i ; :: according to WAYBEL_0:def_12 ::_thesis: for j being Element of N holds ( not i <= j or not N . j in the carrier of L \ X ) let j be Element of N; ::_thesis: ( not i <= j or not N . j in the carrier of L \ X ) assume i <= j ; ::_thesis: not N . j in the carrier of L \ X then N . j in X by A1; hence not N . j in the carrier of L \ X by XBOOLE_0:def_5; ::_thesis: verum end; given i being Element of N such that A2: for j being Element of N st i <= j holds not N . j in the carrier of L \ X ; :: according to WAYBEL_0:def_12 ::_thesis: N is_eventually_in X take i ; :: according to WAYBEL_0:def_11 ::_thesis: for j being Element of N st i <= j holds N . j in X let j be Element of N; ::_thesis: ( i <= j implies N . j in X ) assume i <= j ; ::_thesis: N . j in X then not N . j in the carrier of L \ X by A2; hence N . j in X by XBOOLE_0:def_5; ::_thesis: verum end; theorem :: WAYBEL_0:10 for L being non empty 1-sorted for N being non empty NetStr over L for X being set holds ( N is_often_in X iff not N is_eventually_in the carrier of L \ X ) proof let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L for X being set holds ( N is_often_in X iff not N is_eventually_in the carrier of L \ X ) let N be non empty NetStr over L; ::_thesis: for X being set holds ( N is_often_in X iff not N is_eventually_in the carrier of L \ X ) let X be set ; ::_thesis: ( N is_often_in X iff not N is_eventually_in the carrier of L \ X ) set Y = the carrier of L \ X; thus ( N is_often_in X implies not N is_eventually_in the carrier of L \ X ) ::_thesis: ( not N is_eventually_in the carrier of L \ X implies N is_often_in X ) proof assume A1: for i being Element of N ex j being Element of N st ( i <= j & N . j in X ) ; :: according to WAYBEL_0:def_12 ::_thesis: not N is_eventually_in the carrier of L \ X let i be Element of N; :: according to WAYBEL_0:def_11 ::_thesis: ex j being Element of N st ( i <= j & not N . j in the carrier of L \ X ) consider j being Element of N such that A2: i <= j and A3: N . j in X by A1; take j ; ::_thesis: ( i <= j & not N . j in the carrier of L \ X ) thus ( i <= j & not N . j in the carrier of L \ X ) by A2, A3, XBOOLE_0:def_5; ::_thesis: verum end; assume A4: for i being Element of N ex j being Element of N st ( i <= j & not N . j in the carrier of L \ X ) ; :: according to WAYBEL_0:def_11 ::_thesis: N is_often_in X let i be Element of N; :: according to WAYBEL_0:def_12 ::_thesis: ex j being Element of N st ( i <= j & N . j in X ) consider j being Element of N such that A5: i <= j and A6: not N . j in the carrier of L \ X by A4; take j ; ::_thesis: ( i <= j & N . j in X ) thus ( i <= j & N . j in X ) by A5, A6, XBOOLE_0:def_5; ::_thesis: verum end; scheme :: WAYBEL_0:sch 1 HoldsEventually{ F1() -> non empty RelStr , F2() -> non empty NetStr over F1(), P1[ set ] } : ( F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] } iff ex i being Element of F2() st for j being Element of F2() st i <= j holds P1[F2() . j] ) proof set X = { (F2() . k) where k is Element of F2() : P1[F2() . k] } ; hereby ::_thesis: ( ex i being Element of F2() st for j being Element of F2() st i <= j holds P1[F2() . j] implies F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] } ) assume F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] } ; ::_thesis: ex i being Element of F2() st for j being Element of F2() st i <= j holds P1[F2() . j] then consider i being Element of F2() such that A1: for j being Element of F2() st i <= j holds F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } by Def11; take i = i; ::_thesis: for j being Element of F2() st i <= j holds P1[F2() . j] let j be Element of F2(); ::_thesis: ( i <= j implies P1[F2() . j] ) assume i <= j ; ::_thesis: P1[F2() . j] then F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } by A1; then ex k being Element of F2() st ( F2() . j = F2() . k & P1[F2() . k] ) ; hence P1[F2() . j] ; ::_thesis: verum end; given i being Element of F2() such that A2: for j being Element of F2() st i <= j holds P1[F2() . j] ; ::_thesis: F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] } take i ; :: according to WAYBEL_0:def_11 ::_thesis: for j being Element of F2() st i <= j holds F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } let j be Element of F2(); ::_thesis: ( i <= j implies F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } ) assume i <= j ; ::_thesis: F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } then P1[F2() . j] by A2; hence F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } ; ::_thesis: verum end; definition let L be non empty RelStr ; let N be non empty NetStr over L; attrN is eventually-directed means :Def13: :: WAYBEL_0:def 13 for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } ; attrN is eventually-filtered means :Def14: :: WAYBEL_0:def 14 for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } ; end; :: deftheorem Def13 defines eventually-directed WAYBEL_0:def_13_:_ for L being non empty RelStr for N being non empty NetStr over L holds ( N is eventually-directed iff for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } ); :: deftheorem Def14 defines eventually-filtered WAYBEL_0:def_14_:_ for L being non empty RelStr for N being non empty NetStr over L holds ( N is eventually-filtered iff for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } ); theorem Th11: :: WAYBEL_0:11 for L being non empty RelStr for N being non empty NetStr over L holds ( N is eventually-directed iff for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i <= N . k ) proof let L be non empty RelStr ; ::_thesis: for N being non empty NetStr over L holds ( N is eventually-directed iff for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i <= N . k ) let N be non empty NetStr over L; ::_thesis: ( N is eventually-directed iff for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i <= N . k ) A1: now__::_thesis:_for_i_being_Element_of_N_holds_ (_N_is_eventually_in__{__(N_._j)_where_j_is_Element_of_N_:_S1[N_._j]__}__iff_ex_k_being_Element_of_N_st_ for_l_being_Element_of_N_st_k_<=_l_holds_ S1[N_._l]_) let i be Element of N; ::_thesis: ( N is_eventually_in { (N . j) where j is Element of N : S1[N . j] } iff ex k being Element of N st for l being Element of N st k <= l holds S1[N . l] ) defpred S1[ Element of L] means N . i <= $1; thus ( N is_eventually_in { (N . j) where j is Element of N : S1[N . j] } iff ex k being Element of N st for l being Element of N st k <= l holds S1[N . l] ) from WAYBEL_0:sch_1(); ::_thesis: verum end; hereby ::_thesis: ( ( for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i <= N . k ) implies N is eventually-directed ) assume A2: N is eventually-directed ; ::_thesis: for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i <= N . k let i be Element of N; ::_thesis: ex j being Element of N st for k being Element of N st j <= k holds N . i <= N . k N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } by A2, Def13; hence ex j being Element of N st for k being Element of N st j <= k holds N . i <= N . k by A1; ::_thesis: verum end; assume A3: for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i <= N . k ; ::_thesis: N is eventually-directed let i be Element of N; :: according to WAYBEL_0:def_13 ::_thesis: N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } ex j being Element of N st for k being Element of N st j <= k holds N . i <= N . k by A3; hence N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } by A1; ::_thesis: verum end; theorem Th12: :: WAYBEL_0:12 for L being non empty RelStr for N being non empty NetStr over L holds ( N is eventually-filtered iff for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i >= N . k ) proof let L be non empty RelStr ; ::_thesis: for N being non empty NetStr over L holds ( N is eventually-filtered iff for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i >= N . k ) let N be non empty NetStr over L; ::_thesis: ( N is eventually-filtered iff for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i >= N . k ) A1: now__::_thesis:_for_i_being_Element_of_N_holds_ (_N_is_eventually_in__{__(N_._j)_where_j_is_Element_of_N_:_S1[N_._j]__}__iff_ex_k_being_Element_of_N_st_ for_l_being_Element_of_N_st_k_<=_l_holds_ S1[N_._l]_) let i be Element of N; ::_thesis: ( N is_eventually_in { (N . j) where j is Element of N : S1[N . j] } iff ex k being Element of N st for l being Element of N st k <= l holds S1[N . l] ) defpred S1[ Element of L] means N . i >= $1; thus ( N is_eventually_in { (N . j) where j is Element of N : S1[N . j] } iff ex k being Element of N st for l being Element of N st k <= l holds S1[N . l] ) from WAYBEL_0:sch_1(); ::_thesis: verum end; hereby ::_thesis: ( ( for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i >= N . k ) implies N is eventually-filtered ) assume A2: N is eventually-filtered ; ::_thesis: for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i >= N . k let i be Element of N; ::_thesis: ex j being Element of N st for k being Element of N st j <= k holds N . i >= N . k N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } by A2, Def14; hence ex j being Element of N st for k being Element of N st j <= k holds N . i >= N . k by A1; ::_thesis: verum end; assume A3: for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N . i >= N . k ; ::_thesis: N is eventually-filtered let i be Element of N; :: according to WAYBEL_0:def_14 ::_thesis: N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } ex j being Element of N st for k being Element of N st j <= k holds N . i >= N . k by A3; hence N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } by A1; ::_thesis: verum end; registration let L be non empty RelStr ; cluster non empty directed monotone -> eventually-directed for NetStr over L; coherence for b1 being prenet of L st b1 is monotone holds b1 is eventually-directed proof let N be prenet of L; ::_thesis: ( N is monotone implies N is eventually-directed ) assume A1: for i, j being Element of N st i <= j holds for a, b being Element of L st a = (netmap (N,L)) . i & b = (netmap (N,L)) . j holds a <= b ; :: according to ORDERS_3:def_5,WAYBEL_0:def_9 ::_thesis: N is eventually-directed now__::_thesis:_for_i_being_Element_of_N_ex_j_being_Element_of_N_st_ for_k_being_Element_of_N_st_j_<=_k_holds_ N_._i_<=_N_._k let i be Element of N; ::_thesis: ex j being Element of N st for k being Element of N st j <= k holds N . i <= N . k take j = i; ::_thesis: for k being Element of N st j <= k holds N . i <= N . k let k be Element of N; ::_thesis: ( j <= k implies N . i <= N . k ) assume j <= k ; ::_thesis: N . i <= N . k hence N . i <= N . k by A1; ::_thesis: verum end; hence N is eventually-directed by Th11; ::_thesis: verum end; cluster non empty directed antitone -> eventually-filtered for NetStr over L; coherence for b1 being prenet of L st b1 is antitone holds b1 is eventually-filtered proof let N be prenet of L; ::_thesis: ( N is antitone implies N is eventually-filtered ) assume A2: for i, j being Element of N st i <= j holds for a, b being Element of L st a = (netmap (N,L)) . i & b = (netmap (N,L)) . j holds a >= b ; :: according to WAYBEL_0:def_5,WAYBEL_0:def_10 ::_thesis: N is eventually-filtered now__::_thesis:_for_i_being_Element_of_N_ex_j_being_Element_of_N_st_ for_k_being_Element_of_N_st_j_<=_k_holds_ N_._i_>=_N_._k let i be Element of N; ::_thesis: ex j being Element of N st for k being Element of N st j <= k holds N . i >= N . k take j = i; ::_thesis: for k being Element of N st j <= k holds N . i >= N . k let k be Element of N; ::_thesis: ( j <= k implies N . i >= N . k ) assume j <= k ; ::_thesis: N . i >= N . k hence N . i >= N . k by A2; ::_thesis: verum end; hence N is eventually-filtered by Th12; ::_thesis: verum end; end; registration let L be non empty reflexive RelStr ; cluster non empty strict directed monotone antitone for NetStr over L; existence ex b1 being prenet of L st ( b1 is monotone & b1 is antitone & b1 is strict ) proof set J = the non empty upper-bounded Poset; set x = the Element of L; set M = the carrier of the non empty upper-bounded Poset --> the Element of L; reconsider M = the carrier of the non empty upper-bounded Poset --> the Element of L as Function of the carrier of the non empty upper-bounded Poset, the carrier of L ; set N = NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #); A1: RelStr(# the carrier of NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #), the InternalRel of NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #) #) = RelStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset #) ; [#] the non empty upper-bounded Poset = [#] NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #) ; then [#] NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #) is directed by A1, Th3; then reconsider N = NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #) as prenet of L by Def6; take N ; ::_thesis: ( N is monotone & N is antitone & N is strict ) thus N is monotone ::_thesis: ( N is antitone & N is strict ) proof let i, j be Element of N; :: according to ORDERS_3:def_5,WAYBEL_0:def_9 ::_thesis: ( not i <= j or for b1, b2 being Element of the carrier of L holds ( not b1 = (netmap (N,L)) . i or not b2 = (netmap (N,L)) . j or b1 <= b2 ) ) assume i <= j ; ::_thesis: for b1, b2 being Element of the carrier of L holds ( not b1 = (netmap (N,L)) . i or not b2 = (netmap (N,L)) . j or b1 <= b2 ) let a, b be Element of L; ::_thesis: ( not a = (netmap (N,L)) . i or not b = (netmap (N,L)) . j or a <= b ) assume that A2: a = (netmap (N,L)) . i and A3: b = (netmap (N,L)) . j ; ::_thesis: a <= b A4: a = the Element of L by A2, FUNCOP_1:7; the Element of L <= the Element of L ; hence a <= b by A3, A4, FUNCOP_1:7; ::_thesis: verum end; thus N is antitone ::_thesis: N is strict proof let i, j be Element of N; :: according to WAYBEL_0:def_5,WAYBEL_0:def_10 ::_thesis: ( i <= j implies for a, b being Element of L st a = (netmap (N,L)) . i & b = (netmap (N,L)) . j holds a >= b ) assume i <= j ; ::_thesis: for a, b being Element of L st a = (netmap (N,L)) . i & b = (netmap (N,L)) . j holds a >= b let a, b be Element of L; ::_thesis: ( a = (netmap (N,L)) . i & b = (netmap (N,L)) . j implies a >= b ) assume that A5: a = (netmap (N,L)) . i and A6: b = (netmap (N,L)) . j ; ::_thesis: a >= b A7: a = the Element of L by A5, FUNCOP_1:7; the Element of L <= the Element of L ; hence a >= b by A6, A7, FUNCOP_1:7; ::_thesis: verum end; thus N is strict ; ::_thesis: verum end; end; begin definition let L be RelStr ; let X be Subset of L; func downarrow X -> Subset of L means :Def15: :: WAYBEL_0:def 15 for x being Element of L holds ( x in it iff ex y being Element of L st ( y >= x & y in X ) ); existence ex b1 being Subset of L st for x being Element of L holds ( x in b1 iff ex y being Element of L st ( y >= x & y in X ) ) proof defpred S1[ set ] means ex a, y being Element of L st ( a = $1 & y >= a & y in X ); consider S being set such that A1: for x being set holds ( x in S iff ( x in the carrier of L & S1[x] ) ) from XBOOLE_0:sch_1(); S c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in the carrier of L ) thus ( not x in S or x in the carrier of L ) by A1; ::_thesis: verum end; then reconsider S = S as Subset of L ; take S ; ::_thesis: for x being Element of L holds ( x in S iff ex y being Element of L st ( y >= x & y in X ) ) let x be Element of L; ::_thesis: ( x in S iff ex y being Element of L st ( y >= x & y in X ) ) hereby ::_thesis: ( ex y being Element of L st ( y >= x & y in X ) implies x in S ) assume x in S ; ::_thesis: ex y being Element of L st ( y >= x & y in X ) then ex a, y being Element of L st ( a = x & y >= a & y in X ) by A1; hence ex y being Element of L st ( y >= x & y in X ) ; ::_thesis: verum end; thus ( ex y being Element of L st ( y >= x & y in X ) implies x in S ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of L st ( for x being Element of L holds ( x in b1 iff ex y being Element of L st ( y >= x & y in X ) ) ) & ( for x being Element of L holds ( x in b2 iff ex y being Element of L st ( y >= x & y in X ) ) ) holds b1 = b2 proof let S1, S2 be Subset of L; ::_thesis: ( ( for x being Element of L holds ( x in S1 iff ex y being Element of L st ( y >= x & y in X ) ) ) & ( for x being Element of L holds ( x in S2 iff ex y being Element of L st ( y >= x & y in X ) ) ) implies S1 = S2 ) assume that A2: for x being Element of L holds ( x in S1 iff ex y being Element of L st ( y >= x & y in X ) ) and A3: for x being Element of L holds ( x in S2 iff ex y being Element of L st ( y >= x & y in X ) ) ; ::_thesis: S1 = S2 thus S1 c= S2 :: according to XBOOLE_0:def_10 ::_thesis: S2 c= S1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S1 or x in S2 ) assume A4: x in S1 ; ::_thesis: x in S2 then reconsider x = x as Element of L ; ex y being Element of L st ( y >= x & y in X ) by A2, A4; hence x in S2 by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S2 or x in S1 ) assume A5: x in S2 ; ::_thesis: x in S1 then reconsider x = x as Element of L ; ex y being Element of L st ( y >= x & y in X ) by A3, A5; hence x in S1 by A2; ::_thesis: verum end; func uparrow X -> Subset of L means :Def16: :: WAYBEL_0:def 16 for x being Element of L holds ( x in it iff ex y being Element of L st ( y <= x & y in X ) ); existence ex b1 being Subset of L st for x being Element of L holds ( x in b1 iff ex y being Element of L st ( y <= x & y in X ) ) proof defpred S1[ set ] means ex a, y being Element of L st ( a = $1 & y <= a & y in X ); consider S being set such that A6: for x being set holds ( x in S iff ( x in the carrier of L & S1[x] ) ) from XBOOLE_0:sch_1(); S c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in the carrier of L ) thus ( not x in S or x in the carrier of L ) by A6; ::_thesis: verum end; then reconsider S = S as Subset of L ; take S ; ::_thesis: for x being Element of L holds ( x in S iff ex y being Element of L st ( y <= x & y in X ) ) let x be Element of L; ::_thesis: ( x in S iff ex y being Element of L st ( y <= x & y in X ) ) hereby ::_thesis: ( ex y being Element of L st ( y <= x & y in X ) implies x in S ) assume x in S ; ::_thesis: ex y being Element of L st ( y <= x & y in X ) then ex a, y being Element of L st ( a = x & y <= a & y in X ) by A6; hence ex y being Element of L st ( y <= x & y in X ) ; ::_thesis: verum end; thus ( ex y being Element of L st ( y <= x & y in X ) implies x in S ) by A6; ::_thesis: verum end; correctness uniqueness for b1, b2 being Subset of L st ( for x being Element of L holds ( x in b1 iff ex y being Element of L st ( y <= x & y in X ) ) ) & ( for x being Element of L holds ( x in b2 iff ex y being Element of L st ( y <= x & y in X ) ) ) holds b1 = b2; proof let S1, S2 be Subset of L; ::_thesis: ( ( for x being Element of L holds ( x in S1 iff ex y being Element of L st ( y <= x & y in X ) ) ) & ( for x being Element of L holds ( x in S2 iff ex y being Element of L st ( y <= x & y in X ) ) ) implies S1 = S2 ) assume that A7: for x being Element of L holds ( x in S1 iff ex y being Element of L st ( y <= x & y in X ) ) and A8: for x being Element of L holds ( x in S2 iff ex y being Element of L st ( y <= x & y in X ) ) ; ::_thesis: S1 = S2 thus S1 c= S2 :: according to XBOOLE_0:def_10 ::_thesis: S2 c= S1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S1 or x in S2 ) assume A9: x in S1 ; ::_thesis: x in S2 then reconsider x = x as Element of L ; ex y being Element of L st ( y <= x & y in X ) by A7, A9; hence x in S2 by A8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S2 or x in S1 ) assume A10: x in S2 ; ::_thesis: x in S1 then reconsider x = x as Element of L ; ex y being Element of L st ( y <= x & y in X ) by A8, A10; hence x in S1 by A7; ::_thesis: verum end; end; :: deftheorem Def15 defines downarrow WAYBEL_0:def_15_:_ for L being RelStr for X, b3 being Subset of L holds ( b3 = downarrow X iff for x being Element of L holds ( x in b3 iff ex y being Element of L st ( y >= x & y in X ) ) ); :: deftheorem Def16 defines uparrow WAYBEL_0:def_16_:_ for L being RelStr for X, b3 being Subset of L holds ( b3 = uparrow X iff for x being Element of L holds ( x in b3 iff ex y being Element of L st ( y <= x & y in X ) ) ); theorem Th13: :: WAYBEL_0:13 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for X being Subset of L1 for Y being Subset of L2 st X = Y holds ( downarrow X = downarrow Y & uparrow X = uparrow Y ) proof let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X being Subset of L1 for Y being Subset of L2 st X = Y holds ( downarrow X = downarrow Y & uparrow X = uparrow Y ) ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X being Subset of L1 for Y being Subset of L2 st X = Y holds ( downarrow X = downarrow Y & uparrow X = uparrow Y ) let X be Subset of L1; ::_thesis: for Y being Subset of L2 st X = Y holds ( downarrow X = downarrow Y & uparrow X = uparrow Y ) let Y be Subset of L2; ::_thesis: ( X = Y implies ( downarrow X = downarrow Y & uparrow X = uparrow Y ) ) assume A2: X = Y ; ::_thesis: ( downarrow X = downarrow Y & uparrow X = uparrow Y ) thus downarrow X c= downarrow Y :: according to XBOOLE_0:def_10 ::_thesis: ( downarrow Y c= downarrow X & uparrow X = uparrow Y ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow X or x in downarrow Y ) assume A3: x in downarrow X ; ::_thesis: x in downarrow Y then reconsider x = x as Element of L1 ; reconsider x9 = x as Element of L2 by A1; consider y being Element of L1 such that A4: y >= x and A5: y in X by A3, Def15; reconsider y9 = y as Element of L2 by A1; y9 >= x9 by A1, A4, YELLOW_0:1; hence x in downarrow Y by A2, A5, Def15; ::_thesis: verum end; thus downarrow Y c= downarrow X ::_thesis: uparrow X = uparrow Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow Y or x in downarrow X ) assume A6: x in downarrow Y ; ::_thesis: x in downarrow X then reconsider x = x as Element of L2 ; reconsider x9 = x as Element of L1 by A1; consider y being Element of L2 such that A7: y >= x and A8: y in Y by A6, Def15; reconsider y9 = y as Element of L1 by A1; y9 >= x9 by A1, A7, YELLOW_0:1; hence x in downarrow X by A2, A8, Def15; ::_thesis: verum end; thus uparrow X c= uparrow Y :: according to XBOOLE_0:def_10 ::_thesis: uparrow Y c= uparrow X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow X or x in uparrow Y ) assume A9: x in uparrow X ; ::_thesis: x in uparrow Y then reconsider x = x as Element of L1 ; reconsider x9 = x as Element of L2 by A1; consider y being Element of L1 such that A10: y <= x and A11: y in X by A9, Def16; reconsider y9 = y as Element of L2 by A1; y9 <= x9 by A1, A10, YELLOW_0:1; hence x in uparrow Y by A2, A11, Def16; ::_thesis: verum end; thus uparrow Y c= uparrow X ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow Y or x in uparrow X ) assume A12: x in uparrow Y ; ::_thesis: x in uparrow X then reconsider x = x as Element of L2 ; reconsider x9 = x as Element of L1 by A1; consider y being Element of L2 such that A13: y <= x and A14: y in Y by A12, Def16; reconsider y9 = y as Element of L1 by A1; y9 <= x9 by A1, A13, YELLOW_0:1; hence x in uparrow X by A2, A14, Def16; ::_thesis: verum end; end; theorem Th14: :: WAYBEL_0:14 for L being non empty RelStr for X being Subset of L holds downarrow X = { x where x is Element of L : ex y being Element of L st ( x <= y & y in X ) } proof let L be non empty RelStr ; ::_thesis: for X being Subset of L holds downarrow X = { x where x is Element of L : ex y being Element of L st ( x <= y & y in X ) } let X be Subset of L; ::_thesis: downarrow X = { x where x is Element of L : ex y being Element of L st ( x <= y & y in X ) } set Y = { x where x is Element of L : ex y being Element of L st ( x <= y & y in X ) } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { x where x is Element of L : ex y being Element of L st ( x <= y & y in X ) } c= downarrow X let x be set ; ::_thesis: ( x in downarrow X implies x in { x where x is Element of L : ex y being Element of L st ( x <= y & y in X ) } ) assume A1: x in downarrow X ; ::_thesis: x in { x where x is Element of L : ex y being Element of L st ( x <= y & y in X ) } then reconsider y = x as Element of L ; ex z being Element of L st ( z >= y & z in X ) by A1, Def15; hence x in { x where x is Element of L : ex y being Element of L st ( x <= y & y in X ) } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of L : ex y being Element of L st ( x <= y & y in X ) } or x in downarrow X ) assume x in { x where x is Element of L : ex y being Element of L st ( x <= y & y in X ) } ; ::_thesis: x in downarrow X then ex a being Element of L st ( a = x & ex y being Element of L st ( a <= y & y in X ) ) ; hence x in downarrow X by Def15; ::_thesis: verum end; theorem Th15: :: WAYBEL_0:15 for L being non empty RelStr for X being Subset of L holds uparrow X = { x where x is Element of L : ex y being Element of L st ( x >= y & y in X ) } proof let L be non empty RelStr ; ::_thesis: for X being Subset of L holds uparrow X = { x where x is Element of L : ex y being Element of L st ( x >= y & y in X ) } let X be Subset of L; ::_thesis: uparrow X = { x where x is Element of L : ex y being Element of L st ( x >= y & y in X ) } set Y = { x where x is Element of L : ex y being Element of L st ( x >= y & y in X ) } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { x where x is Element of L : ex y being Element of L st ( x >= y & y in X ) } c= uparrow X let x be set ; ::_thesis: ( x in uparrow X implies x in { x where x is Element of L : ex y being Element of L st ( x >= y & y in X ) } ) assume A1: x in uparrow X ; ::_thesis: x in { x where x is Element of L : ex y being Element of L st ( x >= y & y in X ) } then reconsider y = x as Element of L ; ex z being Element of L st ( z <= y & z in X ) by A1, Def16; hence x in { x where x is Element of L : ex y being Element of L st ( x >= y & y in X ) } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of L : ex y being Element of L st ( x >= y & y in X ) } or x in uparrow X ) assume x in { x where x is Element of L : ex y being Element of L st ( x >= y & y in X ) } ; ::_thesis: x in uparrow X then ex a being Element of L st ( a = x & ex y being Element of L st ( a >= y & y in X ) ) ; hence x in uparrow X by Def16; ::_thesis: verum end; registration let L be non empty reflexive RelStr ; let X be non empty Subset of L; cluster downarrow X -> non empty ; coherence not downarrow X is empty proof set x = the Element of X; reconsider x9 = the Element of X as Element of L ; x9 <= x9 ; hence not downarrow X is empty by Def15; ::_thesis: verum end; cluster uparrow X -> non empty ; coherence not uparrow X is empty proof set x = the Element of X; reconsider x9 = the Element of X as Element of L ; x9 <= x9 ; hence not uparrow X is empty by Def16; ::_thesis: verum end; end; theorem Th16: :: WAYBEL_0:16 for L being reflexive RelStr for X being Subset of L holds ( X c= downarrow X & X c= uparrow X ) proof let L be reflexive RelStr ; ::_thesis: for X being Subset of L holds ( X c= downarrow X & X c= uparrow X ) let X be Subset of L; ::_thesis: ( X c= downarrow X & X c= uparrow X ) A1: the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def_2; hereby :: according to TARSKI:def_3 ::_thesis: X c= uparrow X let x be set ; ::_thesis: ( x in X implies x in downarrow X ) assume A2: x in X ; ::_thesis: x in downarrow X then reconsider y = x as Element of L ; [y,y] in the InternalRel of L by A1, A2, RELAT_2:def_1; then y <= y by ORDERS_2:def_5; hence x in downarrow X by A2, Def15; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in uparrow X ) assume A3: x in X ; ::_thesis: x in uparrow X then reconsider y = x as Element of L ; [y,y] in the InternalRel of L by A1, A3, RELAT_2:def_1; then y <= y by ORDERS_2:def_5; hence x in uparrow X by A3, Def16; ::_thesis: verum end; definition let L be non empty RelStr ; let x be Element of L; func downarrow x -> Subset of L equals :: WAYBEL_0:def 17 downarrow {x}; correctness coherence downarrow {x} is Subset of L; ; func uparrow x -> Subset of L equals :: WAYBEL_0:def 18 uparrow {x}; correctness coherence uparrow {x} is Subset of L; ; end; :: deftheorem defines downarrow WAYBEL_0:def_17_:_ for L being non empty RelStr for x being Element of L holds downarrow x = downarrow {x}; :: deftheorem defines uparrow WAYBEL_0:def_18_:_ for L being non empty RelStr for x being Element of L holds uparrow x = uparrow {x}; theorem Th17: :: WAYBEL_0:17 for L being non empty RelStr for x, y being Element of L holds ( y in downarrow x iff y <= x ) proof let L be non empty RelStr ; ::_thesis: for x, y being Element of L holds ( y in downarrow x iff y <= x ) let x, y be Element of L; ::_thesis: ( y in downarrow x iff y <= x ) A1: downarrow x = { z where z is Element of L : ex v being Element of L st ( z <= v & v in {x} ) } by Th14; then ( y in downarrow x iff ex z being Element of L st ( y = z & ex v being Element of L st ( z <= v & v in {x} ) ) ) ; hence ( y in downarrow x implies y <= x ) by TARSKI:def_1; ::_thesis: ( y <= x implies y in downarrow x ) x in {x} by TARSKI:def_1; hence ( y <= x implies y in downarrow x ) by A1; ::_thesis: verum end; theorem Th18: :: WAYBEL_0:18 for L being non empty RelStr for x, y being Element of L holds ( y in uparrow x iff x <= y ) proof let L be non empty RelStr ; ::_thesis: for x, y being Element of L holds ( y in uparrow x iff x <= y ) let x, y be Element of L; ::_thesis: ( y in uparrow x iff x <= y ) A1: uparrow x = { z where z is Element of L : ex v being Element of L st ( z >= v & v in {x} ) } by Th15; then ( y in uparrow x iff ex z being Element of L st ( y = z & ex v being Element of L st ( z >= v & v in {x} ) ) ) ; hence ( y in uparrow x implies y >= x ) by TARSKI:def_1; ::_thesis: ( x <= y implies y in uparrow x ) x in {x} by TARSKI:def_1; hence ( x <= y implies y in uparrow x ) by A1; ::_thesis: verum end; theorem :: WAYBEL_0:19 for L being non empty reflexive antisymmetric RelStr for x, y being Element of L st downarrow x = downarrow y holds x = y proof let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for x, y being Element of L st downarrow x = downarrow y holds x = y let x, y be Element of L; ::_thesis: ( downarrow x = downarrow y implies x = y ) reconsider x9 = x, y9 = y as Element of L ; A1: x9 <= x9 ; A2: y9 <= y9 ; assume A3: downarrow x = downarrow y ; ::_thesis: x = y then A4: y in downarrow x by A2, Th17; x in downarrow y by A1, A3, Th17; then A5: x9 <= y9 by Th17; x9 >= y9 by A4, Th17; hence x = y by A5, ORDERS_2:2; ::_thesis: verum end; theorem :: WAYBEL_0:20 for L being non empty reflexive antisymmetric RelStr for x, y being Element of L st uparrow x = uparrow y holds x = y proof let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for x, y being Element of L st uparrow x = uparrow y holds x = y let x, y be Element of L; ::_thesis: ( uparrow x = uparrow y implies x = y ) reconsider x9 = x, y9 = y as Element of L ; A1: x9 <= x9 ; A2: y9 <= y9 ; assume A3: uparrow x = uparrow y ; ::_thesis: x = y then A4: y in uparrow x by A2, Th18; A5: x in uparrow y by A1, A3, Th18; A6: x9 <= y9 by A4, Th18; x9 >= y9 by A5, Th18; hence x = y by A6, ORDERS_2:2; ::_thesis: verum end; theorem Th21: :: WAYBEL_0:21 for L being non empty transitive RelStr for x, y being Element of L st x <= y holds downarrow x c= downarrow y proof let L be non empty transitive RelStr ; ::_thesis: for x, y being Element of L st x <= y holds downarrow x c= downarrow y let x, y be Element of L; ::_thesis: ( x <= y implies downarrow x c= downarrow y ) assume A1: x <= y ; ::_thesis: downarrow x c= downarrow y let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in downarrow x or z in downarrow y ) assume A2: z in downarrow x ; ::_thesis: z in downarrow y then reconsider z = z as Element of L ; z <= x by A2, Th17; then z <= y by A1, ORDERS_2:3; hence z in downarrow y by Th17; ::_thesis: verum end; theorem Th22: :: WAYBEL_0:22 for L being non empty transitive RelStr for x, y being Element of L st x <= y holds uparrow y c= uparrow x proof let L be non empty transitive RelStr ; ::_thesis: for x, y being Element of L st x <= y holds uparrow y c= uparrow x let x, y be Element of L; ::_thesis: ( x <= y implies uparrow y c= uparrow x ) assume A1: x <= y ; ::_thesis: uparrow y c= uparrow x let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in uparrow y or z in uparrow x ) assume A2: z in uparrow y ; ::_thesis: z in uparrow x then reconsider z = z as Element of L ; y <= z by A2, Th18; then x <= z by A1, ORDERS_2:3; hence z in uparrow x by Th18; ::_thesis: verum end; registration let L be non empty reflexive RelStr ; let x be Element of L; cluster downarrow x -> non empty directed ; coherence ( not downarrow x is empty & downarrow x is directed ) proof reconsider x9 = x as Element of L ; thus not downarrow x is empty ; ::_thesis: downarrow x is directed let z, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( z in downarrow x & y in downarrow x implies ex z being Element of L st ( z in downarrow x & z <= z & y <= z ) ) assume that A1: z in downarrow x and A2: y in downarrow x ; ::_thesis: ex z being Element of L st ( z in downarrow x & z <= z & y <= z ) take x9 ; ::_thesis: ( x9 in downarrow x & z <= x9 & y <= x9 ) x9 <= x9 ; hence ( x9 in downarrow x & z <= x9 & y <= x9 ) by A1, A2, Th17; ::_thesis: verum end; cluster uparrow x -> non empty filtered ; coherence ( not uparrow x is empty & uparrow x is filtered ) proof reconsider x9 = x as Element of L ; thus not uparrow x is empty ; ::_thesis: uparrow x is filtered let z, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( z in uparrow x & y in uparrow x implies ex z being Element of L st ( z in uparrow x & z <= z & z <= y ) ) assume that A3: z in uparrow x and A4: y in uparrow x ; ::_thesis: ex z being Element of L st ( z in uparrow x & z <= z & z <= y ) take x9 ; ::_thesis: ( x9 in uparrow x & x9 <= z & x9 <= y ) x9 <= x9 ; hence ( x9 in uparrow x & x9 <= z & x9 <= y ) by A3, A4, Th18; ::_thesis: verum end; end; definition let L be RelStr ; let X be Subset of L; attrX is lower means :Def19: :: WAYBEL_0:def 19 for x, y being Element of L st x in X & y <= x holds y in X; attrX is upper means :Def20: :: WAYBEL_0:def 20 for x, y being Element of L st x in X & x <= y holds y in X; end; :: deftheorem Def19 defines lower WAYBEL_0:def_19_:_ for L being RelStr for X being Subset of L holds ( X is lower iff for x, y being Element of L st x in X & y <= x holds y in X ); :: deftheorem Def20 defines upper WAYBEL_0:def_20_:_ for L being RelStr for X being Subset of L holds ( X is upper iff for x, y being Element of L st x in X & x <= y holds y in X ); registration let L be RelStr ; cluster lower upper for Element of K10( the carrier of L); existence ex b1 being Subset of L st ( b1 is lower & b1 is upper ) proof the carrier of L c= the carrier of L ; then reconsider S = the carrier of L as Subset of L ; take S ; ::_thesis: ( S is lower & S is upper ) thus S is lower ::_thesis: S is upper proof let x be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: for y being Element of L st x in S & y <= x holds y in S thus for y being Element of L st x in S & y <= x holds y in S ; ::_thesis: verum end; let x be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: for y being Element of L st x in S & x <= y holds y in S thus for y being Element of L st x in S & x <= y holds y in S ; ::_thesis: verum end; end; theorem Th23: :: WAYBEL_0:23 for L being RelStr for X being Subset of L holds ( X is lower iff downarrow X c= X ) proof let L be RelStr ; ::_thesis: for X being Subset of L holds ( X is lower iff downarrow X c= X ) let X be Subset of L; ::_thesis: ( X is lower iff downarrow X c= X ) hereby ::_thesis: ( downarrow X c= X implies X is lower ) assume A1: X is lower ; ::_thesis: downarrow X c= X thus downarrow X c= X ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow X or x in X ) assume A2: x in downarrow X ; ::_thesis: x in X then reconsider x9 = x as Element of L ; ex y being Element of L st ( x9 <= y & y in X ) by A2, Def15; hence x in X by A1, Def19; ::_thesis: verum end; end; assume A3: downarrow X c= X ; ::_thesis: X is lower let x, y be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( x in X & y <= x implies y in X ) assume that A4: x in X and A5: y <= x ; ::_thesis: y in X y in downarrow X by A4, A5, Def15; hence y in X by A3; ::_thesis: verum end; theorem Th24: :: WAYBEL_0:24 for L being RelStr for X being Subset of L holds ( X is upper iff uparrow X c= X ) proof let L be RelStr ; ::_thesis: for X being Subset of L holds ( X is upper iff uparrow X c= X ) let X be Subset of L; ::_thesis: ( X is upper iff uparrow X c= X ) hereby ::_thesis: ( uparrow X c= X implies X is upper ) assume A1: X is upper ; ::_thesis: uparrow X c= X thus uparrow X c= X ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow X or x in X ) assume A2: x in uparrow X ; ::_thesis: x in X then reconsider x9 = x as Element of L ; ex y being Element of L st ( x9 >= y & y in X ) by A2, Def16; hence x in X by A1, Def20; ::_thesis: verum end; end; assume A3: uparrow X c= X ; ::_thesis: X is upper let x, y be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( x in X & x <= y implies y in X ) assume that A4: x in X and A5: y >= x ; ::_thesis: y in X y in uparrow X by A4, A5, Def16; hence y in X by A3; ::_thesis: verum end; theorem :: WAYBEL_0:25 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for X1 being Subset of L1 for X2 being Subset of L2 st X1 = X2 holds ( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) ) proof let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X1 being Subset of L1 for X2 being Subset of L2 st X1 = X2 holds ( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) ) ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X1 being Subset of L1 for X2 being Subset of L2 st X1 = X2 holds ( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) ) let X1 be Subset of L1; ::_thesis: for X2 being Subset of L2 st X1 = X2 holds ( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) ) let X2 be Subset of L2; ::_thesis: ( X1 = X2 implies ( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) ) ) assume A2: X1 = X2 ; ::_thesis: ( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) ) hereby ::_thesis: ( X1 is upper implies X2 is upper ) assume A3: X1 is lower ; ::_thesis: X2 is lower A4: downarrow X1 = downarrow X2 by A1, A2, Th13; downarrow X1 c= X1 by A3, Th23; hence X2 is lower by A2, A4, Th23; ::_thesis: verum end; assume A5: X1 is upper ; ::_thesis: X2 is upper A6: uparrow X1 = uparrow X2 by A1, A2, Th13; uparrow X1 c= X1 by A5, Th24; hence X2 is upper by A2, A6, Th24; ::_thesis: verum end; theorem :: WAYBEL_0:26 for L being RelStr for A being Subset-Family of L st ( for X being Subset of L st X in A holds X is lower ) holds union A is lower Subset of L proof let L be RelStr ; ::_thesis: for A being Subset-Family of L st ( for X being Subset of L st X in A holds X is lower ) holds union A is lower Subset of L let A be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in A holds X is lower ) implies union A is lower Subset of L ) assume A1: for X being Subset of L st X in A holds X is lower ; ::_thesis: union A is lower Subset of L reconsider A = A as Subset-Family of L ; reconsider X = union A as Subset of L ; X is lower proof let x, y be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( x in X & y <= x implies y in X ) assume x in X ; ::_thesis: ( not y <= x or y in X ) then consider Y being set such that A2: x in Y and A3: Y in A by TARSKI:def_4; reconsider Y = Y as Subset of L by A3; A4: Y is lower by A1, A3; assume y <= x ; ::_thesis: y in X then y in Y by A2, A4, Def19; hence y in X by A3, TARSKI:def_4; ::_thesis: verum end; hence union A is lower Subset of L ; ::_thesis: verum end; theorem Th27: :: WAYBEL_0:27 for L being RelStr for X, Y being Subset of L st X is lower & Y is lower holds ( X /\ Y is lower & X \/ Y is lower ) proof let L be RelStr ; ::_thesis: for X, Y being Subset of L st X is lower & Y is lower holds ( X /\ Y is lower & X \/ Y is lower ) let X, Y be Subset of L; ::_thesis: ( X is lower & Y is lower implies ( X /\ Y is lower & X \/ Y is lower ) ) assume that A1: for x, y being Element of L st x in X & y <= x holds y in X and A2: for x, y being Element of L st x in Y & y <= x holds y in Y ; :: according to WAYBEL_0:def_19 ::_thesis: ( X /\ Y is lower & X \/ Y is lower ) hereby :: according to WAYBEL_0:def_19 ::_thesis: X \/ Y is lower let x, y be Element of L; ::_thesis: ( x in X /\ Y & y <= x implies y in X /\ Y ) assume A3: x in X /\ Y ; ::_thesis: ( y <= x implies y in X /\ Y ) then A4: x in X by XBOOLE_0:def_4; A5: x in Y by A3, XBOOLE_0:def_4; assume A6: y <= x ; ::_thesis: y in X /\ Y then A7: y in X by A1, A4; y in Y by A2, A5, A6; hence y in X /\ Y by A7, XBOOLE_0:def_4; ::_thesis: verum end; let x, y be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( x in X \/ Y & y <= x implies y in X \/ Y ) assume x in X \/ Y ; ::_thesis: ( not y <= x or y in X \/ Y ) then A8: ( x in X or x in Y ) by XBOOLE_0:def_3; assume y <= x ; ::_thesis: y in X \/ Y then ( y in X or y in Y ) by A1, A2, A8; hence y in X \/ Y by XBOOLE_0:def_3; ::_thesis: verum end; theorem :: WAYBEL_0:28 for L being RelStr for A being Subset-Family of L st ( for X being Subset of L st X in A holds X is upper ) holds union A is upper Subset of L proof let L be RelStr ; ::_thesis: for A being Subset-Family of L st ( for X being Subset of L st X in A holds X is upper ) holds union A is upper Subset of L let A be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in A holds X is upper ) implies union A is upper Subset of L ) assume A1: for X being Subset of L st X in A holds X is upper ; ::_thesis: union A is upper Subset of L reconsider A = A as Subset-Family of L ; reconsider X = union A as Subset of L ; X is upper proof let x, y be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( x in X & x <= y implies y in X ) assume x in X ; ::_thesis: ( not x <= y or y in X ) then consider Y being set such that A2: x in Y and A3: Y in A by TARSKI:def_4; reconsider Y = Y as Subset of L by A3; A4: Y is upper by A1, A3; assume y >= x ; ::_thesis: y in X then y in Y by A2, A4, Def20; hence y in X by A3, TARSKI:def_4; ::_thesis: verum end; hence union A is upper Subset of L ; ::_thesis: verum end; theorem Th29: :: WAYBEL_0:29 for L being RelStr for X, Y being Subset of L st X is upper & Y is upper holds ( X /\ Y is upper & X \/ Y is upper ) proof let L be RelStr ; ::_thesis: for X, Y being Subset of L st X is upper & Y is upper holds ( X /\ Y is upper & X \/ Y is upper ) let X, Y be Subset of L; ::_thesis: ( X is upper & Y is upper implies ( X /\ Y is upper & X \/ Y is upper ) ) assume that A1: for x, y being Element of L st x in X & y >= x holds y in X and A2: for x, y being Element of L st x in Y & y >= x holds y in Y ; :: according to WAYBEL_0:def_20 ::_thesis: ( X /\ Y is upper & X \/ Y is upper ) hereby :: according to WAYBEL_0:def_20 ::_thesis: X \/ Y is upper let x, y be Element of L; ::_thesis: ( x in X /\ Y & y >= x implies y in X /\ Y ) assume A3: x in X /\ Y ; ::_thesis: ( y >= x implies y in X /\ Y ) then A4: x in X by XBOOLE_0:def_4; A5: x in Y by A3, XBOOLE_0:def_4; assume A6: y >= x ; ::_thesis: y in X /\ Y then A7: y in X by A1, A4; y in Y by A2, A5, A6; hence y in X /\ Y by A7, XBOOLE_0:def_4; ::_thesis: verum end; let x, y be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( x in X \/ Y & x <= y implies y in X \/ Y ) assume x in X \/ Y ; ::_thesis: ( not x <= y or y in X \/ Y ) then A8: ( x in X or x in Y ) by XBOOLE_0:def_3; assume y >= x ; ::_thesis: y in X \/ Y then ( y in X or y in Y ) by A1, A2, A8; hence y in X \/ Y by XBOOLE_0:def_3; ::_thesis: verum end; registration let L be non empty transitive RelStr ; let X be Subset of L; cluster downarrow X -> lower ; coherence downarrow X is lower proof let y, z be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( y in downarrow X & z <= y implies z in downarrow X ) assume y in downarrow X ; ::_thesis: ( not z <= y or z in downarrow X ) then consider x being Element of L such that A1: y <= x and A2: x in X by Def15; assume z <= y ; ::_thesis: z in downarrow X then z <= x by A1, ORDERS_2:3; hence z in downarrow X by A2, Def15; ::_thesis: verum end; cluster uparrow X -> upper ; coherence uparrow X is upper proof let y, z be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( y in uparrow X & y <= z implies z in uparrow X ) assume y in uparrow X ; ::_thesis: ( not y <= z or z in uparrow X ) then consider x being Element of L such that A3: y >= x and A4: x in X by Def16; assume z >= y ; ::_thesis: z in uparrow X then z >= x by A3, ORDERS_2:3; hence z in uparrow X by A4, Def16; ::_thesis: verum end; end; registration let L be non empty transitive RelStr ; let x be Element of L; cluster downarrow x -> lower ; coherence downarrow x is lower ; cluster uparrow x -> upper ; coherence uparrow x is upper ; end; registration let L be non empty RelStr ; cluster [#] L -> lower upper ; coherence ( [#] L is lower & [#] L is upper ) proof set X = [#] L; thus for x, y being Element of L st x in [#] L & y <= x holds y in [#] L ; :: according to WAYBEL_0:def_19 ::_thesis: [#] L is upper thus for x, y being Element of L st x in [#] L & x <= y holds y in [#] L ; :: according to WAYBEL_0:def_20 ::_thesis: verum end; end; registration let L be non empty RelStr ; cluster non empty lower upper for Element of K10( the carrier of L); existence ex b1 being Subset of L st ( not b1 is empty & b1 is lower & b1 is upper ) proof take [#] L ; ::_thesis: ( not [#] L is empty & [#] L is lower & [#] L is upper ) thus ( not [#] L is empty & [#] L is lower & [#] L is upper ) ; ::_thesis: verum end; end; registration let L be non empty reflexive transitive RelStr ; cluster non empty directed lower for Element of K10( the carrier of L); existence ex b1 being Subset of L st ( not b1 is empty & b1 is lower & b1 is directed ) proof set x = the Element of L; take downarrow the Element of L ; ::_thesis: ( not downarrow the Element of L is empty & downarrow the Element of L is lower & downarrow the Element of L is directed ) thus ( not downarrow the Element of L is empty & downarrow the Element of L is lower & downarrow the Element of L is directed ) ; ::_thesis: verum end; cluster non empty filtered upper for Element of K10( the carrier of L); existence ex b1 being Subset of L st ( not b1 is empty & b1 is upper & b1 is filtered ) proof set x = the Element of L; take uparrow the Element of L ; ::_thesis: ( not uparrow the Element of L is empty & uparrow the Element of L is upper & uparrow the Element of L is filtered ) thus ( not uparrow the Element of L is empty & uparrow the Element of L is upper & uparrow the Element of L is filtered ) ; ::_thesis: verum end; end; registration let L be with_suprema with_infima Poset; cluster non empty directed filtered lower upper for Element of K10( the carrier of L); existence ex b1 being Subset of L st ( not b1 is empty & b1 is directed & b1 is filtered & b1 is lower & b1 is upper ) proof take [#] L ; ::_thesis: ( not [#] L is empty & [#] L is directed & [#] L is filtered & [#] L is lower & [#] L is upper ) thus ( not [#] L is empty & [#] L is directed & [#] L is filtered & [#] L is lower & [#] L is upper ) ; ::_thesis: verum end; end; theorem Th30: :: WAYBEL_0:30 for L being non empty reflexive transitive RelStr for X being Subset of L holds ( X is directed iff downarrow X is directed ) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L holds ( X is directed iff downarrow X is directed ) let X be Subset of L; ::_thesis: ( X is directed iff downarrow X is directed ) thus ( X is directed implies downarrow X is directed ) ::_thesis: ( downarrow X is directed implies X is directed ) proof assume A1: for x, y being Element of L st x in X & y in X holds ex z being Element of L st ( z in X & x <= z & y <= z ) ; :: according to WAYBEL_0:def_1 ::_thesis: downarrow X is directed let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in downarrow X & y in downarrow X implies ex z being Element of L st ( z in downarrow X & x <= z & y <= z ) ) assume that A2: x in downarrow X and A3: y in downarrow X ; ::_thesis: ex z being Element of L st ( z in downarrow X & x <= z & y <= z ) consider x9 being Element of L such that A4: x <= x9 and A5: x9 in X by A2, Def15; consider y9 being Element of L such that A6: y <= y9 and A7: y9 in X by A3, Def15; consider z being Element of L such that A8: z in X and A9: x9 <= z and A10: y9 <= z by A1, A5, A7; take z ; ::_thesis: ( z in downarrow X & x <= z & y <= z ) z <= z ; hence z in downarrow X by A8, Def15; ::_thesis: ( x <= z & y <= z ) thus ( x <= z & y <= z ) by A4, A6, A9, A10, ORDERS_2:3; ::_thesis: verum end; set Y = downarrow X; assume A11: for x, y being Element of L st x in downarrow X & y in downarrow X holds ex z being Element of L st ( z in downarrow X & x <= z & y <= z ) ; :: according to WAYBEL_0:def_1 ::_thesis: X is directed let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in X & y in X implies ex z being Element of L st ( z in X & x <= z & y <= z ) ) assume that A12: x in X and A13: y in X ; ::_thesis: ex z being Element of L st ( z in X & x <= z & y <= z ) A14: x <= x ; A15: y <= y ; A16: x in downarrow X by A12, A14, Def15; y in downarrow X by A13, A15, Def15; then consider z being Element of L such that A17: z in downarrow X and A18: x <= z and A19: y <= z by A11, A16; consider z9 being Element of L such that A20: z <= z9 and A21: z9 in X by A17, Def15; take z9 ; ::_thesis: ( z9 in X & x <= z9 & y <= z9 ) thus z9 in X by A21; ::_thesis: ( x <= z9 & y <= z9 ) thus ( x <= z9 & y <= z9 ) by A18, A19, A20, ORDERS_2:3; ::_thesis: verum end; registration let L be non empty reflexive transitive RelStr ; let X be directed Subset of L; cluster downarrow X -> directed ; coherence downarrow X is directed by Th30; end; theorem Th31: :: WAYBEL_0:31 for L being non empty reflexive transitive RelStr for X being Subset of L for x being Element of L holds ( x is_>=_than X iff x is_>=_than downarrow X ) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L for x being Element of L holds ( x is_>=_than X iff x is_>=_than downarrow X ) let X be Subset of L; ::_thesis: for x being Element of L holds ( x is_>=_than X iff x is_>=_than downarrow X ) let x be Element of L; ::_thesis: ( x is_>=_than X iff x is_>=_than downarrow X ) thus ( x is_>=_than X implies x is_>=_than downarrow X ) ::_thesis: ( x is_>=_than downarrow X implies x is_>=_than X ) proof assume A1: for y being Element of L st y in X holds x >= y ; :: according to LATTICE3:def_9 ::_thesis: x is_>=_than downarrow X let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in downarrow X or y <= x ) assume y in downarrow X ; ::_thesis: y <= x then consider z being Element of L such that A2: y <= z and A3: z in X by Def15; x >= z by A1, A3; hence y <= x by A2, ORDERS_2:3; ::_thesis: verum end; assume A4: for y being Element of L st y in downarrow X holds x >= y ; :: according to LATTICE3:def_9 ::_thesis: x is_>=_than X let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in X or y <= x ) assume A5: y in X ; ::_thesis: y <= x y <= y ; then y in downarrow X by A5, Def15; hence y <= x by A4; ::_thesis: verum end; theorem Th32: :: WAYBEL_0:32 for L being non empty reflexive transitive RelStr for X being Subset of L holds ( ex_sup_of X,L iff ex_sup_of downarrow X,L ) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L holds ( ex_sup_of X,L iff ex_sup_of downarrow X,L ) let X be Subset of L; ::_thesis: ( ex_sup_of X,L iff ex_sup_of downarrow X,L ) for x being Element of L holds ( x is_>=_than X iff x is_>=_than downarrow X ) by Th31; hence ( ex_sup_of X,L iff ex_sup_of downarrow X,L ) by YELLOW_0:46; ::_thesis: verum end; theorem Th33: :: WAYBEL_0:33 for L being non empty reflexive transitive RelStr for X being Subset of L st ex_sup_of X,L holds sup X = sup (downarrow X) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L st ex_sup_of X,L holds sup X = sup (downarrow X) let X be Subset of L; ::_thesis: ( ex_sup_of X,L implies sup X = sup (downarrow X) ) for x being Element of L holds ( x is_>=_than X iff x is_>=_than downarrow X ) by Th31; hence ( ex_sup_of X,L implies sup X = sup (downarrow X) ) by YELLOW_0:47; ::_thesis: verum end; theorem :: WAYBEL_0:34 for L being non empty Poset for x being Element of L holds ( ex_sup_of downarrow x,L & sup (downarrow x) = x ) proof let L be non empty Poset; ::_thesis: for x being Element of L holds ( ex_sup_of downarrow x,L & sup (downarrow x) = x ) let x be Element of L; ::_thesis: ( ex_sup_of downarrow x,L & sup (downarrow x) = x ) ex_sup_of {x},L by YELLOW_0:38; hence ex_sup_of downarrow x,L by Th32; ::_thesis: sup (downarrow x) = x thus sup (downarrow x) = sup {x} by Th33, YELLOW_0:38 .= x by YELLOW_0:39 ; ::_thesis: verum end; theorem Th35: :: WAYBEL_0:35 for L being non empty reflexive transitive RelStr for X being Subset of L holds ( X is filtered iff uparrow X is filtered ) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L holds ( X is filtered iff uparrow X is filtered ) let X be Subset of L; ::_thesis: ( X is filtered iff uparrow X is filtered ) thus ( X is filtered implies uparrow X is filtered ) ::_thesis: ( uparrow X is filtered implies X is filtered ) proof assume A1: for x, y being Element of L st x in X & y in X holds ex z being Element of L st ( z in X & x >= z & y >= z ) ; :: according to WAYBEL_0:def_2 ::_thesis: uparrow X is filtered let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in uparrow X & y in uparrow X implies ex z being Element of L st ( z in uparrow X & z <= x & z <= y ) ) assume that A2: x in uparrow X and A3: y in uparrow X ; ::_thesis: ex z being Element of L st ( z in uparrow X & z <= x & z <= y ) consider x9 being Element of L such that A4: x >= x9 and A5: x9 in X by A2, Def16; consider y9 being Element of L such that A6: y >= y9 and A7: y9 in X by A3, Def16; consider z being Element of L such that A8: z in X and A9: x9 >= z and A10: y9 >= z by A1, A5, A7; take z ; ::_thesis: ( z in uparrow X & z <= x & z <= y ) z >= z by ORDERS_2:1; hence z in uparrow X by A8, Def16; ::_thesis: ( z <= x & z <= y ) thus ( z <= x & z <= y ) by A4, A6, A9, A10, ORDERS_2:3; ::_thesis: verum end; set Y = uparrow X; assume A11: for x, y being Element of L st x in uparrow X & y in uparrow X holds ex z being Element of L st ( z in uparrow X & x >= z & y >= z ) ; :: according to WAYBEL_0:def_2 ::_thesis: X is filtered let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in X & y in X implies ex z being Element of L st ( z in X & z <= x & z <= y ) ) assume that A12: x in X and A13: y in X ; ::_thesis: ex z being Element of L st ( z in X & z <= x & z <= y ) A14: x >= x by ORDERS_2:1; A15: y >= y by ORDERS_2:1; A16: x in uparrow X by A12, A14, Def16; y in uparrow X by A13, A15, Def16; then consider z being Element of L such that A17: z in uparrow X and A18: x >= z and A19: y >= z by A11, A16; consider z9 being Element of L such that A20: z >= z9 and A21: z9 in X by A17, Def16; take z9 ; ::_thesis: ( z9 in X & z9 <= x & z9 <= y ) thus z9 in X by A21; ::_thesis: ( z9 <= x & z9 <= y ) thus ( z9 <= x & z9 <= y ) by A18, A19, A20, ORDERS_2:3; ::_thesis: verum end; registration let L be non empty reflexive transitive RelStr ; let X be filtered Subset of L; cluster uparrow X -> filtered ; coherence uparrow X is filtered by Th35; end; theorem Th36: :: WAYBEL_0:36 for L being non empty reflexive transitive RelStr for X being Subset of L for x being Element of L holds ( x is_<=_than X iff x is_<=_than uparrow X ) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L for x being Element of L holds ( x is_<=_than X iff x is_<=_than uparrow X ) let X be Subset of L; ::_thesis: for x being Element of L holds ( x is_<=_than X iff x is_<=_than uparrow X ) let x be Element of L; ::_thesis: ( x is_<=_than X iff x is_<=_than uparrow X ) thus ( x is_<=_than X implies x is_<=_than uparrow X ) ::_thesis: ( x is_<=_than uparrow X implies x is_<=_than X ) proof assume A1: for y being Element of L st y in X holds x <= y ; :: according to LATTICE3:def_8 ::_thesis: x is_<=_than uparrow X let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in uparrow X or x <= y ) assume y in uparrow X ; ::_thesis: x <= y then consider z being Element of L such that A2: y >= z and A3: z in X by Def16; x <= z by A1, A3; hence x <= y by A2, ORDERS_2:3; ::_thesis: verum end; assume A4: for y being Element of L st y in uparrow X holds x <= y ; :: according to LATTICE3:def_8 ::_thesis: x is_<=_than X let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in X or x <= y ) assume A5: y in X ; ::_thesis: x <= y y <= y ; then y in uparrow X by A5, Def16; hence x <= y by A4; ::_thesis: verum end; theorem Th37: :: WAYBEL_0:37 for L being non empty reflexive transitive RelStr for X being Subset of L holds ( ex_inf_of X,L iff ex_inf_of uparrow X,L ) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L holds ( ex_inf_of X,L iff ex_inf_of uparrow X,L ) let X be Subset of L; ::_thesis: ( ex_inf_of X,L iff ex_inf_of uparrow X,L ) for x being Element of L holds ( x is_<=_than X iff x is_<=_than uparrow X ) by Th36; hence ( ex_inf_of X,L iff ex_inf_of uparrow X,L ) by YELLOW_0:48; ::_thesis: verum end; theorem Th38: :: WAYBEL_0:38 for L being non empty reflexive transitive RelStr for X being Subset of L st ex_inf_of X,L holds inf X = inf (uparrow X) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L st ex_inf_of X,L holds inf X = inf (uparrow X) let X be Subset of L; ::_thesis: ( ex_inf_of X,L implies inf X = inf (uparrow X) ) for x being Element of L holds ( x is_<=_than X iff x is_<=_than uparrow X ) by Th36; hence ( ex_inf_of X,L implies inf X = inf (uparrow X) ) by YELLOW_0:49; ::_thesis: verum end; theorem :: WAYBEL_0:39 for L being non empty Poset for x being Element of L holds ( ex_inf_of uparrow x,L & inf (uparrow x) = x ) proof let L be non empty Poset; ::_thesis: for x being Element of L holds ( ex_inf_of uparrow x,L & inf (uparrow x) = x ) let x be Element of L; ::_thesis: ( ex_inf_of uparrow x,L & inf (uparrow x) = x ) ex_inf_of {x},L by YELLOW_0:38; hence ex_inf_of uparrow x,L by Th37; ::_thesis: inf (uparrow x) = x thus inf (uparrow x) = inf {x} by Th38, YELLOW_0:38 .= x by YELLOW_0:39 ; ::_thesis: verum end; begin definition let L be non empty reflexive transitive RelStr ; mode Ideal of L is non empty directed lower Subset of L; mode Filter of L is non empty filtered upper Subset of L; end; theorem Th40: :: WAYBEL_0:40 for L being antisymmetric with_suprema RelStr for X being lower Subset of L holds ( X is directed iff for x, y being Element of L st x in X & y in X holds x "\/" y in X ) proof let L be antisymmetric with_suprema RelStr ; ::_thesis: for X being lower Subset of L holds ( X is directed iff for x, y being Element of L st x in X & y in X holds x "\/" y in X ) let X be lower Subset of L; ::_thesis: ( X is directed iff for x, y being Element of L st x in X & y in X holds x "\/" y in X ) thus ( X is directed implies for x, y being Element of L st x in X & y in X holds x "\/" y in X ) ::_thesis: ( ( for x, y being Element of L st x in X & y in X holds x "\/" y in X ) implies X is directed ) proof assume A1: for x, y being Element of L st x in X & y in X holds ex z being Element of L st ( z in X & x <= z & y <= z ) ; :: according to WAYBEL_0:def_1 ::_thesis: for x, y being Element of L st x in X & y in X holds x "\/" y in X let x, y be Element of L; ::_thesis: ( x in X & y in X implies x "\/" y in X ) assume that A2: x in X and A3: y in X ; ::_thesis: x "\/" y in X consider z being Element of L such that A4: z in X and A5: x <= z and A6: y <= z by A1, A2, A3; x "\/" y <= z by A5, A6, YELLOW_0:22; hence x "\/" y in X by A4, Def19; ::_thesis: verum end; assume A7: for x, y being Element of L st x in X & y in X holds x "\/" y in X ; ::_thesis: X is directed let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in X & y in X implies ex z being Element of L st ( z in X & x <= z & y <= z ) ) assume that A8: x in X and A9: y in X ; ::_thesis: ex z being Element of L st ( z in X & x <= z & y <= z ) A10: x <= x "\/" y by YELLOW_0:22; y <= x "\/" y by YELLOW_0:22; hence ex z being Element of L st ( z in X & x <= z & y <= z ) by A7, A8, A9, A10; ::_thesis: verum end; theorem Th41: :: WAYBEL_0:41 for L being antisymmetric with_infima RelStr for X being upper Subset of L holds ( X is filtered iff for x, y being Element of L st x in X & y in X holds x "/\" y in X ) proof let L be antisymmetric with_infima RelStr ; ::_thesis: for X being upper Subset of L holds ( X is filtered iff for x, y being Element of L st x in X & y in X holds x "/\" y in X ) let X be upper Subset of L; ::_thesis: ( X is filtered iff for x, y being Element of L st x in X & y in X holds x "/\" y in X ) thus ( X is filtered implies for x, y being Element of L st x in X & y in X holds x "/\" y in X ) ::_thesis: ( ( for x, y being Element of L st x in X & y in X holds x "/\" y in X ) implies X is filtered ) proof assume A1: for x, y being Element of L st x in X & y in X holds ex z being Element of L st ( z in X & x >= z & y >= z ) ; :: according to WAYBEL_0:def_2 ::_thesis: for x, y being Element of L st x in X & y in X holds x "/\" y in X let x, y be Element of L; ::_thesis: ( x in X & y in X implies x "/\" y in X ) assume that A2: x in X and A3: y in X ; ::_thesis: x "/\" y in X consider z being Element of L such that A4: z in X and A5: x >= z and A6: y >= z by A1, A2, A3; x "/\" y >= z by A5, A6, YELLOW_0:23; hence x "/\" y in X by A4, Def20; ::_thesis: verum end; assume A7: for x, y being Element of L st x in X & y in X holds x "/\" y in X ; ::_thesis: X is filtered let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in X & y in X implies ex z being Element of L st ( z in X & z <= x & z <= y ) ) assume that A8: x in X and A9: y in X ; ::_thesis: ex z being Element of L st ( z in X & z <= x & z <= y ) A10: x >= x "/\" y by YELLOW_0:23; y >= x "/\" y by YELLOW_0:23; hence ex z being Element of L st ( z in X & z <= x & z <= y ) by A7, A8, A9, A10; ::_thesis: verum end; theorem Th42: :: WAYBEL_0:42 for L being with_suprema Poset for X being non empty lower Subset of L holds ( X is directed iff for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in X ) proof let L be with_suprema Poset; ::_thesis: for X being non empty lower Subset of L holds ( X is directed iff for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in X ) let X be non empty lower Subset of L; ::_thesis: ( X is directed iff for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in X ) thus ( X is directed implies for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in X ) ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in X ) implies X is directed ) proof assume A1: X is directed ; ::_thesis: for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in X let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "\/" (Y,L) in X ) assume A2: Y <> {} ; ::_thesis: "\/" (Y,L) in X consider z being Element of L such that A3: z in X and A4: Y is_<=_than z by A1, Th1; Y c= the carrier of L by XBOOLE_1:1; then ex_sup_of Y,L by A2, YELLOW_0:54; then "\/" (Y,L) <= z by A4, YELLOW_0:30; hence "\/" (Y,L) in X by A3, Def19; ::_thesis: verum end; assume A5: for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in X ; ::_thesis: X is directed set x = the Element of X; reconsider x = the Element of X as Element of L ; now__::_thesis:_for_Y_being_finite_Subset_of_X_ex_x_being_Element_of_L_st_ (_x_in_X_&_x_is_>=_than_Y_) let Y be finite Subset of X; ::_thesis: ex x being Element of L st ( b2 in X & b2 is_>=_than x ) percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: ex x being Element of L st ( b2 in X & b2 is_>=_than x ) then x is_>=_than Y by YELLOW_0:6; hence ex x being Element of L st ( x in X & x is_>=_than Y ) ; ::_thesis: verum end; supposeA6: Y <> {} ; ::_thesis: ex x being Element of L st ( b2 in X & b2 is_>=_than x ) Y c= the carrier of L by XBOOLE_1:1; then ex_sup_of Y,L by A6, YELLOW_0:54; then "\/" (Y,L) is_>=_than Y by YELLOW_0:30; hence ex x being Element of L st ( x in X & x is_>=_than Y ) by A5, A6; ::_thesis: verum end; end; end; hence X is directed by Th1; ::_thesis: verum end; theorem Th43: :: WAYBEL_0:43 for L being with_infima Poset for X being non empty upper Subset of L holds ( X is filtered iff for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in X ) proof let L be with_infima Poset; ::_thesis: for X being non empty upper Subset of L holds ( X is filtered iff for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in X ) let X be non empty upper Subset of L; ::_thesis: ( X is filtered iff for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in X ) thus ( X is filtered implies for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in X ) ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in X ) implies X is filtered ) proof assume A1: X is filtered ; ::_thesis: for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in X let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "/\" (Y,L) in X ) assume A2: Y <> {} ; ::_thesis: "/\" (Y,L) in X consider z being Element of L such that A3: z in X and A4: Y is_>=_than z by A1, Th2; Y c= the carrier of L by XBOOLE_1:1; then ex_inf_of Y,L by A2, YELLOW_0:55; then "/\" (Y,L) >= z by A4, YELLOW_0:31; hence "/\" (Y,L) in X by A3, Def20; ::_thesis: verum end; assume A5: for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in X ; ::_thesis: X is filtered set x = the Element of X; reconsider x = the Element of X as Element of L ; now__::_thesis:_for_Y_being_finite_Subset_of_X_ex_x_being_Element_of_L_st_ (_x_in_X_&_x_is_<=_than_Y_) let Y be finite Subset of X; ::_thesis: ex x being Element of L st ( b2 in X & b2 is_<=_than x ) percases ( Y = {} or Y <> {} ) ; suppose Y = {} ; ::_thesis: ex x being Element of L st ( b2 in X & b2 is_<=_than x ) then x is_<=_than Y by YELLOW_0:6; hence ex x being Element of L st ( x in X & x is_<=_than Y ) ; ::_thesis: verum end; supposeA6: Y <> {} ; ::_thesis: ex x being Element of L st ( b2 in X & b2 is_<=_than x ) Y c= the carrier of L by XBOOLE_1:1; then ex_inf_of Y,L by A6, YELLOW_0:55; then "/\" (Y,L) is_<=_than Y by YELLOW_0:31; hence ex x being Element of L st ( x in X & x is_<=_than Y ) by A5, A6; ::_thesis: verum end; end; end; hence X is filtered by Th2; ::_thesis: verum end; theorem :: WAYBEL_0:44 for L being non empty antisymmetric RelStr st ( L is with_suprema or L is with_infima ) holds for X, Y being Subset of L st X is lower & X is directed & Y is lower & Y is directed holds X /\ Y is directed proof let L be non empty antisymmetric RelStr ; ::_thesis: ( ( L is with_suprema or L is with_infima ) implies for X, Y being Subset of L st X is lower & X is directed & Y is lower & Y is directed holds X /\ Y is directed ) assume A1: ( L is with_suprema or L is with_infima ) ; ::_thesis: for X, Y being Subset of L st X is lower & X is directed & Y is lower & Y is directed holds X /\ Y is directed let X, Y be Subset of L; ::_thesis: ( X is lower & X is directed & Y is lower & Y is directed implies X /\ Y is directed ) assume that A2: ( X is lower & X is directed ) and A3: ( Y is lower & Y is directed ) ; ::_thesis: X /\ Y is directed A4: X /\ Y is lower by A2, A3, Th27; percases ( L is with_suprema or L is with_infima ) by A1; supposeA5: L is with_suprema ; ::_thesis: X /\ Y is directed now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_X_/\_Y_&_y_in_X_/\_Y_holds_ x_"\/"_y_in_X_/\_Y let x, y be Element of L; ::_thesis: ( x in X /\ Y & y in X /\ Y implies x "\/" y in X /\ Y ) assume that A6: x in X /\ Y and A7: y in X /\ Y ; ::_thesis: x "\/" y in X /\ Y A8: x in X by A6, XBOOLE_0:def_4; A9: x in Y by A6, XBOOLE_0:def_4; A10: y in X by A7, XBOOLE_0:def_4; A11: y in Y by A7, XBOOLE_0:def_4; A12: x "\/" y in X by A2, A5, A8, A10, Th40; x "\/" y in Y by A3, A5, A9, A11, Th40; hence x "\/" y in X /\ Y by A12, XBOOLE_0:def_4; ::_thesis: verum end; hence X /\ Y is directed by A4, A5, Th40; ::_thesis: verum end; supposeA13: L is with_infima ; ::_thesis: X /\ Y is directed let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in X /\ Y & y in X /\ Y implies ex z being Element of L st ( z in X /\ Y & x <= z & y <= z ) ) assume that A14: x in X /\ Y and A15: y in X /\ Y ; ::_thesis: ex z being Element of L st ( z in X /\ Y & x <= z & y <= z ) A16: x in X by A14, XBOOLE_0:def_4; A17: x in Y by A14, XBOOLE_0:def_4; A18: y in X by A15, XBOOLE_0:def_4; A19: y in Y by A15, XBOOLE_0:def_4; consider zx being Element of L such that A20: zx in X and A21: x <= zx and A22: y <= zx by A2, A16, A18, Def1; consider zy being Element of L such that A23: zy in Y and A24: x <= zy and A25: y <= zy by A3, A17, A19, Def1; take z = zx "/\" zy; ::_thesis: ( z in X /\ Y & x <= z & y <= z ) A26: z <= zx by A13, YELLOW_0:23; A27: z <= zy by A13, YELLOW_0:23; A28: z in X by A2, A20, A26, Def19; z in Y by A3, A23, A27, Def19; hence z in X /\ Y by A28, XBOOLE_0:def_4; ::_thesis: ( x <= z & y <= z ) thus ( x <= z & y <= z ) by A13, A21, A22, A24, A25, YELLOW_0:23; ::_thesis: verum end; end; end; theorem :: WAYBEL_0:45 for L being non empty antisymmetric RelStr st ( L is with_suprema or L is with_infima ) holds for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds X /\ Y is filtered proof let L be non empty antisymmetric RelStr ; ::_thesis: ( ( L is with_suprema or L is with_infima ) implies for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds X /\ Y is filtered ) assume A1: ( L is with_suprema or L is with_infima ) ; ::_thesis: for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds X /\ Y is filtered let X, Y be Subset of L; ::_thesis: ( X is upper & X is filtered & Y is upper & Y is filtered implies X /\ Y is filtered ) assume that A2: ( X is upper & X is filtered ) and A3: ( Y is upper & Y is filtered ) ; ::_thesis: X /\ Y is filtered A4: X /\ Y is upper by A2, A3, Th29; percases ( L is with_infima or L is with_suprema ) by A1; supposeA5: L is with_infima ; ::_thesis: X /\ Y is filtered now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_X_/\_Y_&_y_in_X_/\_Y_holds_ x_"/\"_y_in_X_/\_Y let x, y be Element of L; ::_thesis: ( x in X /\ Y & y in X /\ Y implies x "/\" y in X /\ Y ) assume that A6: x in X /\ Y and A7: y in X /\ Y ; ::_thesis: x "/\" y in X /\ Y A8: x in X by A6, XBOOLE_0:def_4; A9: x in Y by A6, XBOOLE_0:def_4; A10: y in X by A7, XBOOLE_0:def_4; A11: y in Y by A7, XBOOLE_0:def_4; A12: x "/\" y in X by A2, A5, A8, A10, Th41; x "/\" y in Y by A3, A5, A9, A11, Th41; hence x "/\" y in X /\ Y by A12, XBOOLE_0:def_4; ::_thesis: verum end; hence X /\ Y is filtered by A4, A5, Th41; ::_thesis: verum end; supposeA13: L is with_suprema ; ::_thesis: X /\ Y is filtered let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in X /\ Y & y in X /\ Y implies ex z being Element of L st ( z in X /\ Y & z <= x & z <= y ) ) assume that A14: x in X /\ Y and A15: y in X /\ Y ; ::_thesis: ex z being Element of L st ( z in X /\ Y & z <= x & z <= y ) A16: x in X by A14, XBOOLE_0:def_4; A17: x in Y by A14, XBOOLE_0:def_4; A18: y in X by A15, XBOOLE_0:def_4; A19: y in Y by A15, XBOOLE_0:def_4; consider zx being Element of L such that A20: zx in X and A21: x >= zx and A22: y >= zx by A2, A16, A18, Def2; consider zy being Element of L such that A23: zy in Y and A24: x >= zy and A25: y >= zy by A3, A17, A19, Def2; take z = zx "\/" zy; ::_thesis: ( z in X /\ Y & z <= x & z <= y ) A26: z >= zx by A13, YELLOW_0:22; A27: z >= zy by A13, YELLOW_0:22; A28: z in X by A2, A20, A26, Def20; z in Y by A3, A23, A27, Def20; hence z in X /\ Y by A28, XBOOLE_0:def_4; ::_thesis: ( z <= x & z <= y ) thus ( z <= x & z <= y ) by A13, A21, A22, A24, A25, YELLOW_0:22; ::_thesis: verum end; end; end; theorem :: WAYBEL_0:46 for L being RelStr for A being Subset-Family of L st ( for X being Subset of L st X in A holds X is directed ) & ( for X, Y being Subset of L st X in A & Y in A holds ex Z being Subset of L st ( Z in A & X \/ Y c= Z ) ) holds for X being Subset of L st X = union A holds X is directed proof let L be RelStr ; ::_thesis: for A being Subset-Family of L st ( for X being Subset of L st X in A holds X is directed ) & ( for X, Y being Subset of L st X in A & Y in A holds ex Z being Subset of L st ( Z in A & X \/ Y c= Z ) ) holds for X being Subset of L st X = union A holds X is directed let A be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in A holds X is directed ) & ( for X, Y being Subset of L st X in A & Y in A holds ex Z being Subset of L st ( Z in A & X \/ Y c= Z ) ) implies for X being Subset of L st X = union A holds X is directed ) assume that A1: for X being Subset of L st X in A holds X is directed and A2: for X, Y being Subset of L st X in A & Y in A holds ex Z being Subset of L st ( Z in A & X \/ Y c= Z ) ; ::_thesis: for X being Subset of L st X = union A holds X is directed let Z be Subset of L; ::_thesis: ( Z = union A implies Z is directed ) assume A3: Z = union A ; ::_thesis: Z is directed let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in Z & y in Z implies ex z being Element of L st ( z in Z & x <= z & y <= z ) ) assume x in Z ; ::_thesis: ( not y in Z or ex z being Element of L st ( z in Z & x <= z & y <= z ) ) then consider X being set such that A4: x in X and A5: X in A by A3, TARSKI:def_4; assume y in Z ; ::_thesis: ex z being Element of L st ( z in Z & x <= z & y <= z ) then consider Y being set such that A6: y in Y and A7: Y in A by A3, TARSKI:def_4; reconsider X = X, Y = Y as Subset of L by A5, A7; consider W being Subset of L such that A8: W in A and A9: X \/ Y c= W by A2, A5, A7; A10: X c= X \/ Y by XBOOLE_1:7; A11: Y c= X \/ Y by XBOOLE_1:7; A12: x in X \/ Y by A4, A10; A13: y in X \/ Y by A6, A11; W is directed by A1, A8; then consider z being Element of L such that A14: z in W and A15: x <= z and A16: y <= z by A9, A12, A13, Def1; take z ; ::_thesis: ( z in Z & x <= z & y <= z ) thus ( z in Z & x <= z & y <= z ) by A3, A8, A14, A15, A16, TARSKI:def_4; ::_thesis: verum end; theorem :: WAYBEL_0:47 for L being RelStr for A being Subset-Family of L st ( for X being Subset of L st X in A holds X is filtered ) & ( for X, Y being Subset of L st X in A & Y in A holds ex Z being Subset of L st ( Z in A & X \/ Y c= Z ) ) holds for X being Subset of L st X = union A holds X is filtered proof let L be RelStr ; ::_thesis: for A being Subset-Family of L st ( for X being Subset of L st X in A holds X is filtered ) & ( for X, Y being Subset of L st X in A & Y in A holds ex Z being Subset of L st ( Z in A & X \/ Y c= Z ) ) holds for X being Subset of L st X = union A holds X is filtered let A be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in A holds X is filtered ) & ( for X, Y being Subset of L st X in A & Y in A holds ex Z being Subset of L st ( Z in A & X \/ Y c= Z ) ) implies for X being Subset of L st X = union A holds X is filtered ) assume that A1: for X being Subset of L st X in A holds X is filtered and A2: for X, Y being Subset of L st X in A & Y in A holds ex Z being Subset of L st ( Z in A & X \/ Y c= Z ) ; ::_thesis: for X being Subset of L st X = union A holds X is filtered let Z be Subset of L; ::_thesis: ( Z = union A implies Z is filtered ) assume A3: Z = union A ; ::_thesis: Z is filtered let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in Z & y in Z implies ex z being Element of L st ( z in Z & z <= x & z <= y ) ) assume x in Z ; ::_thesis: ( not y in Z or ex z being Element of L st ( z in Z & z <= x & z <= y ) ) then consider X being set such that A4: x in X and A5: X in A by A3, TARSKI:def_4; assume y in Z ; ::_thesis: ex z being Element of L st ( z in Z & z <= x & z <= y ) then consider Y being set such that A6: y in Y and A7: Y in A by A3, TARSKI:def_4; reconsider X = X, Y = Y as Subset of L by A5, A7; consider W being Subset of L such that A8: W in A and A9: X \/ Y c= W by A2, A5, A7; A10: X c= X \/ Y by XBOOLE_1:7; A11: Y c= X \/ Y by XBOOLE_1:7; A12: x in X \/ Y by A4, A10; A13: y in X \/ Y by A6, A11; W is filtered by A1, A8; then consider z being Element of L such that A14: z in W and A15: x >= z and A16: y >= z by A9, A12, A13, Def2; take z ; ::_thesis: ( z in Z & z <= x & z <= y ) thus ( z in Z & z <= x & z <= y ) by A3, A8, A14, A15, A16, TARSKI:def_4; ::_thesis: verum end; definition let L be non empty reflexive transitive RelStr ; let I be Ideal of L; attrI is principal means :: WAYBEL_0:def 21 ex x being Element of L st ( x in I & x is_>=_than I ); end; :: deftheorem defines principal WAYBEL_0:def_21_:_ for L being non empty reflexive transitive RelStr for I being Ideal of L holds ( I is principal iff ex x being Element of L st ( x in I & x is_>=_than I ) ); definition let L be non empty reflexive transitive RelStr ; let F be Filter of L; attrF is principal means :: WAYBEL_0:def 22 ex x being Element of L st ( x in F & x is_<=_than F ); end; :: deftheorem defines principal WAYBEL_0:def_22_:_ for L being non empty reflexive transitive RelStr for F being Filter of L holds ( F is principal iff ex x being Element of L st ( x in F & x is_<=_than F ) ); theorem :: WAYBEL_0:48 for L being non empty reflexive transitive RelStr for I being Ideal of L holds ( I is principal iff ex x being Element of L st I = downarrow x ) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for I being Ideal of L holds ( I is principal iff ex x being Element of L st I = downarrow x ) let I be Ideal of L; ::_thesis: ( I is principal iff ex x being Element of L st I = downarrow x ) thus ( I is principal implies ex x being Element of L st I = downarrow x ) ::_thesis: ( ex x being Element of L st I = downarrow x implies I is principal ) proof given x being Element of L such that A1: x in I and A2: x is_>=_than I ; :: according to WAYBEL_0:def_21 ::_thesis: ex x being Element of L st I = downarrow x take x ; ::_thesis: I = downarrow x thus I c= downarrow x :: according to XBOOLE_0:def_10 ::_thesis: downarrow x c= I proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in I or y in downarrow x ) assume A3: y in I ; ::_thesis: y in downarrow x then reconsider y = y as Element of L ; x >= y by A2, A3, LATTICE3:def_9; hence y in downarrow x by Th17; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in downarrow x or z in I ) assume A4: z in downarrow x ; ::_thesis: z in I then reconsider z = z as Element of L ; z <= x by A4, Th17; hence z in I by A1, Def19; ::_thesis: verum end; given x being Element of L such that A5: I = downarrow x ; ::_thesis: I is principal take x ; :: according to WAYBEL_0:def_21 ::_thesis: ( x in I & x is_>=_than I ) x <= x ; hence x in I by A5, Th17; ::_thesis: x is_>=_than I let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in I or y <= x ) thus ( not y in I or y <= x ) by A5, Th17; ::_thesis: verum end; theorem :: WAYBEL_0:49 for L being non empty reflexive transitive RelStr for F being Filter of L holds ( F is principal iff ex x being Element of L st F = uparrow x ) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for F being Filter of L holds ( F is principal iff ex x being Element of L st F = uparrow x ) let I be Filter of L; ::_thesis: ( I is principal iff ex x being Element of L st I = uparrow x ) thus ( I is principal implies ex x being Element of L st I = uparrow x ) ::_thesis: ( ex x being Element of L st I = uparrow x implies I is principal ) proof given x being Element of L such that A1: x in I and A2: x is_<=_than I ; :: according to WAYBEL_0:def_22 ::_thesis: ex x being Element of L st I = uparrow x take x ; ::_thesis: I = uparrow x thus I c= uparrow x :: according to XBOOLE_0:def_10 ::_thesis: uparrow x c= I proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in I or y in uparrow x ) assume A3: y in I ; ::_thesis: y in uparrow x then reconsider y = y as Element of L ; x <= y by A2, A3, LATTICE3:def_8; hence y in uparrow x by Th18; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in uparrow x or z in I ) assume A4: z in uparrow x ; ::_thesis: z in I then reconsider z = z as Element of L ; z >= x by A4, Th18; hence z in I by A1, Def20; ::_thesis: verum end; given x being Element of L such that A5: I = uparrow x ; ::_thesis: I is principal take x ; :: according to WAYBEL_0:def_22 ::_thesis: ( x in I & x is_<=_than I ) x <= x ; hence x in I by A5, Th18; ::_thesis: x is_<=_than I let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in I or x <= y ) thus ( not y in I or x <= y ) by A5, Th18; ::_thesis: verum end; definition let L be non empty reflexive transitive RelStr ; func Ids L -> set equals :: WAYBEL_0:def 23 { X where X is Ideal of L : verum } ; correctness coherence { X where X is Ideal of L : verum } is set ; ; func Filt L -> set equals :: WAYBEL_0:def 24 { X where X is Filter of L : verum } ; correctness coherence { X where X is Filter of L : verum } is set ; ; end; :: deftheorem defines Ids WAYBEL_0:def_23_:_ for L being non empty reflexive transitive RelStr holds Ids L = { X where X is Ideal of L : verum } ; :: deftheorem defines Filt WAYBEL_0:def_24_:_ for L being non empty reflexive transitive RelStr holds Filt L = { X where X is Filter of L : verum } ; definition let L be non empty reflexive transitive RelStr ; func Ids_0 L -> set equals :: WAYBEL_0:def 25 (Ids L) \/ {{}}; correctness coherence (Ids L) \/ {{}} is set ; ; func Filt_0 L -> set equals :: WAYBEL_0:def 26 (Filt L) \/ {{}}; correctness coherence (Filt L) \/ {{}} is set ; ; end; :: deftheorem defines Ids_0 WAYBEL_0:def_25_:_ for L being non empty reflexive transitive RelStr holds Ids_0 L = (Ids L) \/ {{}}; :: deftheorem defines Filt_0 WAYBEL_0:def_26_:_ for L being non empty reflexive transitive RelStr holds Filt_0 L = (Filt L) \/ {{}}; definition let L be non empty RelStr ; let X be Subset of L; set D = { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ; A1: { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } or x in the carrier of L ) assume x in { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ; ::_thesis: x in the carrier of L then ex Y being finite Subset of X st ( x = "\/" (Y,L) & ex_sup_of Y,L ) ; hence x in the carrier of L ; ::_thesis: verum end; func finsups X -> Subset of L equals :: WAYBEL_0:def 27 { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ; correctness coherence { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } is Subset of L; by A1; set D = { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ; A2: { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } or x in the carrier of L ) assume x in { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ; ::_thesis: x in the carrier of L then ex Y being finite Subset of X st ( x = "/\" (Y,L) & ex_inf_of Y,L ) ; hence x in the carrier of L ; ::_thesis: verum end; func fininfs X -> Subset of L equals :: WAYBEL_0:def 28 { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ; correctness coherence { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } is Subset of L; by A2; end; :: deftheorem defines finsups WAYBEL_0:def_27_:_ for L being non empty RelStr for X being Subset of L holds finsups X = { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ; :: deftheorem defines fininfs WAYBEL_0:def_28_:_ for L being non empty RelStr for X being Subset of L holds fininfs X = { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ; registration let L be non empty antisymmetric lower-bounded RelStr ; let X be Subset of L; cluster finsups X -> non empty ; coherence not finsups X is empty proof ex_sup_of {} ,L by YELLOW_0:42; then "\/" (({} X),L) in finsups X ; hence not finsups X is empty ; ::_thesis: verum end; end; registration let L be non empty antisymmetric upper-bounded RelStr ; let X be Subset of L; cluster fininfs X -> non empty ; coherence not fininfs X is empty proof ex_inf_of {} ,L by YELLOW_0:43; then "/\" (({} X),L) in fininfs X ; hence not fininfs X is empty ; ::_thesis: verum end; end; registration let L be non empty reflexive antisymmetric RelStr ; let X be non empty Subset of L; cluster finsups X -> non empty ; coherence not finsups X is empty proof set x = the Element of X; reconsider y = the Element of X as Element of L ; reconsider Z = {y} as finite Subset of X by ZFMISC_1:31; ex_sup_of Z,L by YELLOW_0:38; then "\/" (Z,L) in finsups X ; hence not finsups X is empty ; ::_thesis: verum end; cluster fininfs X -> non empty ; coherence not fininfs X is empty proof set x = the Element of X; reconsider y = the Element of X as Element of L ; reconsider Z = {y} as finite Subset of X by ZFMISC_1:31; ex_inf_of Z,L by YELLOW_0:38; then "/\" (Z,L) in fininfs X ; hence not fininfs X is empty ; ::_thesis: verum end; end; theorem Th50: :: WAYBEL_0:50 for L being non empty reflexive antisymmetric RelStr for X being Subset of L holds ( X c= finsups X & X c= fininfs X ) proof let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for X being Subset of L holds ( X c= finsups X & X c= fininfs X ) let X be Subset of L; ::_thesis: ( X c= finsups X & X c= fininfs X ) hereby :: according to TARSKI:def_3 ::_thesis: X c= fininfs X let x be set ; ::_thesis: ( x in X implies x in finsups X ) assume A1: x in X ; ::_thesis: x in finsups X then reconsider y = x as Element of L ; reconsider Y = {x} as finite Subset of X by A1, ZFMISC_1:31; A2: y = "\/" (Y,L) by YELLOW_0:39; ex_sup_of {y},L by YELLOW_0:38; hence x in finsups X by A2; ::_thesis: verum end; hereby :: according to TARSKI:def_3 ::_thesis: verum let x be set ; ::_thesis: ( x in X implies x in fininfs X ) assume A3: x in X ; ::_thesis: x in fininfs X then reconsider y = x as Element of L ; reconsider Y = {x} as finite Subset of X by A3, ZFMISC_1:31; A4: y = "/\" (Y,L) by YELLOW_0:39; ex_inf_of {y},L by YELLOW_0:38; hence x in fininfs X by A4; ::_thesis: verum end; end; theorem Th51: :: WAYBEL_0:51 for L being non empty transitive RelStr for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ) holds F is directed proof let L be non empty transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ) holds F is directed let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ) implies F is directed ) assume that A1: for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L and A2: for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) and A3: for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ; ::_thesis: F is directed let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in F & y in F implies ex z being Element of L st ( z in F & x <= z & y <= z ) ) assume A4: x in F ; ::_thesis: ( not y in F or ex z being Element of L st ( z in F & x <= z & y <= z ) ) then consider Y1 being finite Subset of X such that A5: ex_sup_of Y1,L and A6: x = "\/" (Y1,L) by A2; assume y in F ; ::_thesis: ex z being Element of L st ( z in F & x <= z & y <= z ) then consider Y2 being finite Subset of X such that A7: ex_sup_of Y2,L and A8: y = "\/" (Y2,L) by A2; take z = "\/" ((Y1 \/ Y2),L); ::_thesis: ( z in F & x <= z & y <= z ) A9: ( ( Y1 = {} & Y2 = {} & {} \/ {} = {} ) or Y1 \/ Y2 <> {} ) ; hence z in F by A3, A4, A6; ::_thesis: ( x <= z & y <= z ) ex_sup_of Y1 \/ Y2,L by A1, A5, A9; hence ( x <= z & y <= z ) by A5, A6, A7, A8, XBOOLE_1:7, YELLOW_0:34; ::_thesis: verum end; registration let L be with_suprema Poset; let X be Subset of L; cluster finsups X -> directed ; coherence finsups X is directed proof reconsider X = X as Subset of L ; A1: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ ex_sup_of_Y,L let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_sup_of Y,L ) Y c= the carrier of L by XBOOLE_1:1; hence ( Y <> {} implies ex_sup_of Y,L ) by YELLOW_0:54; ::_thesis: verum end; A2: now__::_thesis:_for_x_being_Element_of_L_st_x_in_finsups_X_holds_ ex_Y_being_finite_Subset_of_X_st_ (_ex_sup_of_Y,L_&_x_=_"\/"_(Y,L)_) let x be Element of L; ::_thesis: ( x in finsups X implies ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) assume x in finsups X ; ::_thesis: ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) then ex Y being finite Subset of X st ( x = "\/" (Y,L) & ex_sup_of Y,L ) ; hence ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ; ::_thesis: verum end; now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ "\/"_(Y,L)_in_finsups_X let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "\/" (Y,L) in finsups X ) reconsider Z = Y as Subset of L by XBOOLE_1:1; assume Y <> {} ; ::_thesis: "\/" (Y,L) in finsups X then ex_sup_of Z,L by YELLOW_0:54; hence "\/" (Y,L) in finsups X ; ::_thesis: verum end; hence finsups X is directed by A1, A2, Th51; ::_thesis: verum end; end; theorem Th52: :: WAYBEL_0:52 for L being non empty reflexive transitive RelStr for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ) holds for x being Element of L holds ( x is_>=_than X iff x is_>=_than F ) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ) holds for x being Element of L holds ( x is_>=_than X iff x is_>=_than F ) let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ) implies for x being Element of L holds ( x is_>=_than X iff x is_>=_than F ) ) assume that A1: for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L and A2: for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) and A3: for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ; ::_thesis: for x being Element of L holds ( x is_>=_than X iff x is_>=_than F ) let x be Element of L; ::_thesis: ( x is_>=_than X iff x is_>=_than F ) thus ( x is_>=_than X implies x is_>=_than F ) ::_thesis: ( x is_>=_than F implies x is_>=_than X ) proof assume A4: x is_>=_than X ; ::_thesis: x is_>=_than F let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in F or y <= x ) assume y in F ; ::_thesis: y <= x then consider Y being finite Subset of X such that A5: ex_sup_of Y,L and A6: y = "\/" (Y,L) by A2; x is_>=_than Y by A4, YELLOW_0:9; hence y <= x by A5, A6, YELLOW_0:def_9; ::_thesis: verum end; assume A7: x is_>=_than F ; ::_thesis: x is_>=_than X let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in X or y <= x ) assume y in X ; ::_thesis: y <= x then A8: {y} c= X by ZFMISC_1:31; then A9: sup {y} in F by A3; ex_sup_of {y},L by A1, A8; then A10: {y} is_<=_than sup {y} by YELLOW_0:def_9; A11: sup {y} <= x by A7, A9, LATTICE3:def_9; y <= sup {y} by A10, YELLOW_0:7; hence y <= x by A11, ORDERS_2:3; ::_thesis: verum end; theorem Th53: :: WAYBEL_0:53 for L being non empty reflexive transitive RelStr for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ) holds ( ex_sup_of X,L iff ex_sup_of F,L ) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ) holds ( ex_sup_of X,L iff ex_sup_of F,L ) let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ) implies ( ex_sup_of X,L iff ex_sup_of F,L ) ) assume that A1: for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L and A2: for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) and A3: for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ; ::_thesis: ( ex_sup_of X,L iff ex_sup_of F,L ) for x being Element of L holds ( x is_>=_than X iff x is_>=_than F ) by A1, A2, A3, Th52; hence ( ex_sup_of X,L iff ex_sup_of F,L ) by YELLOW_0:46; ::_thesis: verum end; theorem Th54: :: WAYBEL_0:54 for L being non empty reflexive transitive RelStr for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ) & ex_sup_of X,L holds sup F = sup X proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ) & ex_sup_of X,L holds sup F = sup X let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ) & ex_sup_of X,L implies sup F = sup X ) assume that A1: for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L and A2: for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) and A3: for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in F ; ::_thesis: ( not ex_sup_of X,L or sup F = sup X ) for x being Element of L holds ( x is_>=_than X iff x is_>=_than F ) by A1, A2, A3, Th52; hence ( not ex_sup_of X,L or sup F = sup X ) by YELLOW_0:47; ::_thesis: verum end; theorem :: WAYBEL_0:55 for L being with_suprema Poset for X being Subset of L st ( ex_sup_of X,L or L is complete ) holds sup X = sup (finsups X) proof let L be with_suprema Poset; ::_thesis: for X being Subset of L st ( ex_sup_of X,L or L is complete ) holds sup X = sup (finsups X) let X be Subset of L; ::_thesis: ( ( ex_sup_of X,L or L is complete ) implies sup X = sup (finsups X) ) assume ( ex_sup_of X,L or L is complete ) ; ::_thesis: sup X = sup (finsups X) then A1: ex_sup_of X,L by YELLOW_0:17; A2: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ ex_sup_of_Y,L let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_sup_of Y,L ) Y c= the carrier of L by XBOOLE_1:1; hence ( Y <> {} implies ex_sup_of Y,L ) by YELLOW_0:54; ::_thesis: verum end; A3: now__::_thesis:_for_x_being_Element_of_L_st_x_in_finsups_X_holds_ ex_Y_being_finite_Subset_of_X_st_ (_ex_sup_of_Y,L_&_x_=_"\/"_(Y,L)_) let x be Element of L; ::_thesis: ( x in finsups X implies ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) assume x in finsups X ; ::_thesis: ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) then ex Y being finite Subset of X st ( x = "\/" (Y,L) & ex_sup_of Y,L ) ; hence ex Y being finite Subset of X st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ; ::_thesis: verum end; now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ "\/"_(Y,L)_in_finsups_X let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "\/" (Y,L) in finsups X ) reconsider Z = Y as Subset of L by XBOOLE_1:1; assume Y <> {} ; ::_thesis: "\/" (Y,L) in finsups X then ex_sup_of Z,L by YELLOW_0:54; hence "\/" (Y,L) in finsups X ; ::_thesis: verum end; hence sup X = sup (finsups X) by A1, A2, A3, Th54; ::_thesis: verum end; theorem Th56: :: WAYBEL_0:56 for L being non empty transitive RelStr for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ) holds F is filtered proof let L be non empty transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ) holds F is filtered let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ) implies F is filtered ) assume that A1: for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L and A2: for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) and A3: for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ; ::_thesis: F is filtered let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in F & y in F implies ex z being Element of L st ( z in F & z <= x & z <= y ) ) assume A4: x in F ; ::_thesis: ( not y in F or ex z being Element of L st ( z in F & z <= x & z <= y ) ) then consider Y1 being finite Subset of X such that A5: ex_inf_of Y1,L and A6: x = "/\" (Y1,L) by A2; assume y in F ; ::_thesis: ex z being Element of L st ( z in F & z <= x & z <= y ) then consider Y2 being finite Subset of X such that A7: ex_inf_of Y2,L and A8: y = "/\" (Y2,L) by A2; take z = "/\" ((Y1 \/ Y2),L); ::_thesis: ( z in F & z <= x & z <= y ) A9: ( ( Y1 = {} & Y2 = {} & {} \/ {} = {} ) or Y1 \/ Y2 <> {} ) ; hence z in F by A3, A4, A6; ::_thesis: ( z <= x & z <= y ) ex_inf_of Y1 \/ Y2,L by A1, A5, A9; hence ( z <= x & z <= y ) by A5, A6, A7, A8, XBOOLE_1:7, YELLOW_0:35; ::_thesis: verum end; registration let L be with_infima Poset; let X be Subset of L; cluster fininfs X -> filtered ; coherence fininfs X is filtered proof reconsider X = X as Subset of L ; A1: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ ex_inf_of_Y,L let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_inf_of Y,L ) Y c= the carrier of L by XBOOLE_1:1; hence ( Y <> {} implies ex_inf_of Y,L ) by YELLOW_0:55; ::_thesis: verum end; A2: now__::_thesis:_for_x_being_Element_of_L_st_x_in_fininfs_X_holds_ ex_Y_being_finite_Subset_of_X_st_ (_ex_inf_of_Y,L_&_x_=_"/\"_(Y,L)_) let x be Element of L; ::_thesis: ( x in fininfs X implies ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) assume x in fininfs X ; ::_thesis: ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) then ex Y being finite Subset of X st ( x = "/\" (Y,L) & ex_inf_of Y,L ) ; hence ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ; ::_thesis: verum end; now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ "/\"_(Y,L)_in_fininfs_X let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "/\" (Y,L) in fininfs X ) reconsider Z = Y as Subset of L by XBOOLE_1:1; assume Y <> {} ; ::_thesis: "/\" (Y,L) in fininfs X then ex_inf_of Z,L by YELLOW_0:55; hence "/\" (Y,L) in fininfs X ; ::_thesis: verum end; hence fininfs X is filtered by A1, A2, Th56; ::_thesis: verum end; end; theorem Th57: :: WAYBEL_0:57 for L being non empty reflexive transitive RelStr for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ) holds for x being Element of L holds ( x is_<=_than X iff x is_<=_than F ) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ) holds for x being Element of L holds ( x is_<=_than X iff x is_<=_than F ) let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ) implies for x being Element of L holds ( x is_<=_than X iff x is_<=_than F ) ) assume that A1: for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L and A2: for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) and A3: for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ; ::_thesis: for x being Element of L holds ( x is_<=_than X iff x is_<=_than F ) let x be Element of L; ::_thesis: ( x is_<=_than X iff x is_<=_than F ) thus ( x is_<=_than X implies x is_<=_than F ) ::_thesis: ( x is_<=_than F implies x is_<=_than X ) proof assume A4: x is_<=_than X ; ::_thesis: x is_<=_than F let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in F or x <= y ) assume y in F ; ::_thesis: x <= y then consider Y being finite Subset of X such that A5: ex_inf_of Y,L and A6: y = "/\" (Y,L) by A2; x is_<=_than Y by A4, YELLOW_0:9; hence x <= y by A5, A6, YELLOW_0:def_10; ::_thesis: verum end; assume A7: x is_<=_than F ; ::_thesis: x is_<=_than X let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in X or x <= y ) assume y in X ; ::_thesis: x <= y then A8: {y} c= X by ZFMISC_1:31; then A9: inf {y} in F by A3; ex_inf_of {y},L by A1, A8; then A10: {y} is_>=_than inf {y} by YELLOW_0:def_10; A11: inf {y} >= x by A7, A9, LATTICE3:def_8; y >= inf {y} by A10, YELLOW_0:7; hence x <= y by A11, ORDERS_2:3; ::_thesis: verum end; theorem Th58: :: WAYBEL_0:58 for L being non empty reflexive transitive RelStr for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ) holds ( ex_inf_of X,L iff ex_inf_of F,L ) proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ) holds ( ex_inf_of X,L iff ex_inf_of F,L ) let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ) implies ( ex_inf_of X,L iff ex_inf_of F,L ) ) assume that A1: for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L and A2: for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) and A3: for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ; ::_thesis: ( ex_inf_of X,L iff ex_inf_of F,L ) for x being Element of L holds ( x is_<=_than X iff x is_<=_than F ) by A1, A2, A3, Th57; hence ( ex_inf_of X,L iff ex_inf_of F,L ) by YELLOW_0:48; ::_thesis: verum end; theorem Th59: :: WAYBEL_0:59 for L being non empty reflexive transitive RelStr for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ) & ex_inf_of X,L holds inf F = inf X proof let L be non empty reflexive transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ) & ex_inf_of X,L holds inf F = inf X let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L ) & ( for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ) & ex_inf_of X,L implies inf F = inf X ) assume that A1: for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L and A2: for x being Element of L st x in F holds ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) and A3: for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in F ; ::_thesis: ( not ex_inf_of X,L or inf F = inf X ) for x being Element of L holds ( x is_<=_than X iff x is_<=_than F ) by A1, A2, A3, Th57; hence ( not ex_inf_of X,L or inf F = inf X ) by YELLOW_0:49; ::_thesis: verum end; theorem :: WAYBEL_0:60 for L being with_infima Poset for X being Subset of L st ( ex_inf_of X,L or L is complete ) holds inf X = inf (fininfs X) proof let L be with_infima Poset; ::_thesis: for X being Subset of L st ( ex_inf_of X,L or L is complete ) holds inf X = inf (fininfs X) let X be Subset of L; ::_thesis: ( ( ex_inf_of X,L or L is complete ) implies inf X = inf (fininfs X) ) assume ( ex_inf_of X,L or L is complete ) ; ::_thesis: inf X = inf (fininfs X) then A1: ex_inf_of X,L by YELLOW_0:17; A2: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ ex_inf_of_Y,L let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_inf_of Y,L ) Y c= the carrier of L by XBOOLE_1:1; hence ( Y <> {} implies ex_inf_of Y,L ) by YELLOW_0:55; ::_thesis: verum end; A3: now__::_thesis:_for_x_being_Element_of_L_st_x_in_fininfs_X_holds_ ex_Y_being_finite_Subset_of_X_st_ (_ex_inf_of_Y,L_&_x_=_"/\"_(Y,L)_) let x be Element of L; ::_thesis: ( x in fininfs X implies ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ) assume x in fininfs X ; ::_thesis: ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) then ex Y being finite Subset of X st ( x = "/\" (Y,L) & ex_inf_of Y,L ) ; hence ex Y being finite Subset of X st ( ex_inf_of Y,L & x = "/\" (Y,L) ) ; ::_thesis: verum end; now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ "/\"_(Y,L)_in_fininfs_X let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "/\" (Y,L) in fininfs X ) reconsider Z = Y as Subset of L by XBOOLE_1:1; assume Y <> {} ; ::_thesis: "/\" (Y,L) in fininfs X then ex_inf_of Z,L by YELLOW_0:55; hence "/\" (Y,L) in fininfs X ; ::_thesis: verum end; hence inf X = inf (fininfs X) by A1, A2, A3, Th59; ::_thesis: verum end; theorem :: WAYBEL_0:61 for L being with_suprema Poset for X being Subset of L holds ( X c= downarrow (finsups X) & ( for I being Ideal of L st X c= I holds downarrow (finsups X) c= I ) ) proof let L be with_suprema Poset; ::_thesis: for X being Subset of L holds ( X c= downarrow (finsups X) & ( for I being Ideal of L st X c= I holds downarrow (finsups X) c= I ) ) let X be Subset of L; ::_thesis: ( X c= downarrow (finsups X) & ( for I being Ideal of L st X c= I holds downarrow (finsups X) c= I ) ) A1: X c= finsups X by Th50; finsups X c= downarrow (finsups X) by Th16; hence X c= downarrow (finsups X) by A1, XBOOLE_1:1; ::_thesis: for I being Ideal of L st X c= I holds downarrow (finsups X) c= I let I be Ideal of L; ::_thesis: ( X c= I implies downarrow (finsups X) c= I ) assume A2: X c= I ; ::_thesis: downarrow (finsups X) c= I let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow (finsups X) or x in I ) assume A3: x in downarrow (finsups X) ; ::_thesis: x in I then reconsider x = x as Element of L ; consider y being Element of L such that A4: x <= y and A5: y in finsups X by A3, Def15; consider Y being finite Subset of X such that A6: y = "\/" (Y,L) and A7: ex_sup_of Y,L by A5; set i = the Element of I; reconsider i = the Element of I as Element of L ; A8: ex_sup_of {i},L by YELLOW_0:38; A9: sup {i} = i by YELLOW_0:39; A10: now__::_thesis:_(_ex_sup_of_{}_,L_implies_"\/"_({},L)_in_I_) assume ex_sup_of {} ,L ; ::_thesis: "\/" ({},L) in I then "\/" ({},L) <= sup {i} by A8, XBOOLE_1:2, YELLOW_0:34; hence "\/" ({},L) in I by A9, Def19; ::_thesis: verum end; Y c= I by A2, XBOOLE_1:1; then y in I by A6, A7, A10, Th42; hence x in I by A4, Def19; ::_thesis: verum end; theorem :: WAYBEL_0:62 for L being with_infima Poset for X being Subset of L holds ( X c= uparrow (fininfs X) & ( for F being Filter of L st X c= F holds uparrow (fininfs X) c= F ) ) proof let L be with_infima Poset; ::_thesis: for X being Subset of L holds ( X c= uparrow (fininfs X) & ( for F being Filter of L st X c= F holds uparrow (fininfs X) c= F ) ) let X be Subset of L; ::_thesis: ( X c= uparrow (fininfs X) & ( for F being Filter of L st X c= F holds uparrow (fininfs X) c= F ) ) A1: X c= fininfs X by Th50; fininfs X c= uparrow (fininfs X) by Th16; hence X c= uparrow (fininfs X) by A1, XBOOLE_1:1; ::_thesis: for F being Filter of L st X c= F holds uparrow (fininfs X) c= F let I be Filter of L; ::_thesis: ( X c= I implies uparrow (fininfs X) c= I ) assume A2: X c= I ; ::_thesis: uparrow (fininfs X) c= I let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow (fininfs X) or x in I ) assume A3: x in uparrow (fininfs X) ; ::_thesis: x in I then reconsider x = x as Element of L ; consider y being Element of L such that A4: x >= y and A5: y in fininfs X by A3, Def16; consider Y being finite Subset of X such that A6: y = "/\" (Y,L) and A7: ex_inf_of Y,L by A5; set i = the Element of I; reconsider i = the Element of I as Element of L ; A8: ex_inf_of {i},L by YELLOW_0:38; A9: inf {i} = i by YELLOW_0:39; A10: now__::_thesis:_(_ex_inf_of_{}_,L_implies_"/\"_({},L)_in_I_) assume ex_inf_of {} ,L ; ::_thesis: "/\" ({},L) in I then "/\" ({},L) >= inf {i} by A8, XBOOLE_1:2, YELLOW_0:35; hence "/\" ({},L) in I by A9, Def20; ::_thesis: verum end; Y c= I by A2, XBOOLE_1:1; then y in I by A6, A7, A10, Th43; hence x in I by A4, Def20; ::_thesis: verum end; begin definition let L be non empty RelStr ; attrL is connected means :Def29: :: WAYBEL_0:def 29 for x, y being Element of L holds ( x <= y or y <= x ); end; :: deftheorem Def29 defines connected WAYBEL_0:def_29_:_ for L being non empty RelStr holds ( L is connected iff for x, y being Element of L holds ( x <= y or y <= x ) ); registration cluster non empty trivial reflexive -> non empty reflexive connected for RelStr ; coherence for b1 being non empty reflexive RelStr st b1 is trivial holds b1 is connected proof let L be non empty reflexive RelStr ; ::_thesis: ( L is trivial implies L is connected ) assume A1: for x, y being Element of L holds x = y ; :: according to STRUCT_0:def_10 ::_thesis: L is connected let z1, z2 be Element of L; :: according to WAYBEL_0:def_29 ::_thesis: ( z1 <= z2 or z2 <= z1 ) z1 = z2 by A1; hence ( z1 <= z2 or z2 <= z1 ) by ORDERS_2:1; ::_thesis: verum end; end; registration cluster non empty V58() reflexive transitive antisymmetric connected for RelStr ; existence ex b1 being non empty Poset st b1 is connected proof set O = the Order of {0}; take L = RelStr(# {0}, the Order of {0} #); ::_thesis: L is connected let x, y be Element of L; :: according to WAYBEL_0:def_29 ::_thesis: ( x <= y or y <= x ) A1: x = 0 by TARSKI:def_1; y = 0 by TARSKI:def_1; hence ( x <= y or y <= x ) by A1, ORDERS_2:1; ::_thesis: verum end; end; definition mode Chain is non empty connected Poset; end; registration let L be Chain; clusterL ~ -> connected ; coherence L ~ is connected proof let x, y be Element of (L ~); :: according to WAYBEL_0:def_29 ::_thesis: ( x <= y or y <= x ) A1: (~ x) ~ = ~ x ; A2: (~ y) ~ = ~ y ; ( ~ x <= ~ y or ~ x >= ~ y ) by Def29; hence ( x <= y or y <= x ) by A1, A2, LATTICE3:9; ::_thesis: verum end; end; begin definition mode Semilattice is with_infima Poset; mode sup-Semilattice is with_suprema Poset; mode LATTICE is with_suprema with_infima Poset; end; theorem :: WAYBEL_0:63 for L being Semilattice for X being non empty upper Subset of L holds ( X is Filter of L iff subrelstr X is meet-inheriting ) proof let L be Semilattice; ::_thesis: for X being non empty upper Subset of L holds ( X is Filter of L iff subrelstr X is meet-inheriting ) let X be non empty upper Subset of L; ::_thesis: ( X is Filter of L iff subrelstr X is meet-inheriting ) set S = subrelstr X; A1: the carrier of (subrelstr X) = X by YELLOW_0:def_15; hereby ::_thesis: ( subrelstr X is meet-inheriting implies X is Filter of L ) assume A2: X is Filter of L ; ::_thesis: subrelstr X is meet-inheriting thus subrelstr X is meet-inheriting ::_thesis: verum proof let x, y be Element of L; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of (subrelstr X) or not y in the carrier of (subrelstr X) or not ex_inf_of {x,y},L or "/\" ({x,y},L) in the carrier of (subrelstr X) ) assume that A3: x in the carrier of (subrelstr X) and A4: y in the carrier of (subrelstr X) and A5: ex_inf_of {x,y},L ; ::_thesis: "/\" ({x,y},L) in the carrier of (subrelstr X) consider z being Element of L such that A6: z in X and A7: x >= z and A8: y >= z by A1, A2, A3, A4, Def2; z is_<=_than {x,y} by A7, A8, YELLOW_0:8; then z <= inf {x,y} by A5, YELLOW_0:def_10; hence "/\" ({x,y},L) in the carrier of (subrelstr X) by A1, A6, Def20; ::_thesis: verum end; end; assume A9: for x, y being Element of L st x in the carrier of (subrelstr X) & y in the carrier of (subrelstr X) & ex_inf_of {x,y},L holds inf {x,y} in the carrier of (subrelstr X) ; :: according to YELLOW_0:def_16 ::_thesis: X is Filter of L X is filtered proof let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in X & y in X implies ex z being Element of L st ( z in X & z <= x & z <= y ) ) assume that A10: x in X and A11: y in X ; ::_thesis: ex z being Element of L st ( z in X & z <= x & z <= y ) take z = inf {x,y}; ::_thesis: ( z in X & z <= x & z <= y ) A12: z = x "/\" y by YELLOW_0:40; ex_inf_of {x,y},L by YELLOW_0:21; hence ( z in X & z <= x & z <= y ) by A1, A9, A10, A11, A12, YELLOW_0:19; ::_thesis: verum end; hence X is Filter of L ; ::_thesis: verum end; theorem :: WAYBEL_0:64 for L being sup-Semilattice for X being non empty lower Subset of L holds ( X is Ideal of L iff subrelstr X is join-inheriting ) proof let L be sup-Semilattice; ::_thesis: for X being non empty lower Subset of L holds ( X is Ideal of L iff subrelstr X is join-inheriting ) let X be non empty lower Subset of L; ::_thesis: ( X is Ideal of L iff subrelstr X is join-inheriting ) set S = subrelstr X; A1: the carrier of (subrelstr X) = X by YELLOW_0:def_15; hereby ::_thesis: ( subrelstr X is join-inheriting implies X is Ideal of L ) assume A2: X is Ideal of L ; ::_thesis: subrelstr X is join-inheriting thus subrelstr X is join-inheriting ::_thesis: verum proof let x, y be Element of L; :: according to YELLOW_0:def_17 ::_thesis: ( not x in the carrier of (subrelstr X) or not y in the carrier of (subrelstr X) or not ex_sup_of {x,y},L or "\/" ({x,y},L) in the carrier of (subrelstr X) ) assume that A3: x in the carrier of (subrelstr X) and A4: y in the carrier of (subrelstr X) and A5: ex_sup_of {x,y},L ; ::_thesis: "\/" ({x,y},L) in the carrier of (subrelstr X) consider z being Element of L such that A6: z in X and A7: x <= z and A8: y <= z by A1, A2, A3, A4, Def1; z is_>=_than {x,y} by A7, A8, YELLOW_0:8; then z >= sup {x,y} by A5, YELLOW_0:def_9; hence "\/" ({x,y},L) in the carrier of (subrelstr X) by A1, A6, Def19; ::_thesis: verum end; end; assume A9: for x, y being Element of L st x in the carrier of (subrelstr X) & y in the carrier of (subrelstr X) & ex_sup_of {x,y},L holds sup {x,y} in the carrier of (subrelstr X) ; :: according to YELLOW_0:def_17 ::_thesis: X is Ideal of L X is directed proof let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in X & y in X implies ex z being Element of L st ( z in X & x <= z & y <= z ) ) assume that A10: x in X and A11: y in X ; ::_thesis: ex z being Element of L st ( z in X & x <= z & y <= z ) take z = sup {x,y}; ::_thesis: ( z in X & x <= z & y <= z ) A12: z = x "\/" y by YELLOW_0:41; ex_sup_of {x,y},L by YELLOW_0:20; hence ( z in X & x <= z & y <= z ) by A1, A9, A10, A11, A12, YELLOW_0:18; ::_thesis: verum end; hence X is Ideal of L ; ::_thesis: verum end; begin definition let S, T be non empty RelStr ; let f be Function of S,T; let X be Subset of S; predf preserves_inf_of X means :Def30: :: WAYBEL_0:def 30 ( ex_inf_of X,S implies ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) ); predf preserves_sup_of X means :Def31: :: WAYBEL_0:def 31 ( ex_sup_of X,S implies ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) ) ); end; :: deftheorem Def30 defines preserves_inf_of WAYBEL_0:def_30_:_ for S, T being non empty RelStr for f being Function of S,T for X being Subset of S holds ( f preserves_inf_of X iff ( ex_inf_of X,S implies ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) ) ); :: deftheorem Def31 defines preserves_sup_of WAYBEL_0:def_31_:_ for S, T being non empty RelStr for f being Function of S,T for X being Subset of S holds ( f preserves_sup_of X iff ( ex_sup_of X,S implies ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) ) ) ); theorem :: WAYBEL_0:65 for S1, S2, T1, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) & RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds for f being Function of S1,S2 for g being Function of T1,T2 st f = g holds for X being Subset of S1 for Y being Subset of T1 st X = Y holds ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) proof let S1, S2, T1, T2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) & RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) implies for f being Function of S1,S2 for g being Function of T1,T2 st f = g holds for X being Subset of S1 for Y being Subset of T1 st X = Y holds ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) ) assume that A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) and A2: RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: for f being Function of S1,S2 for g being Function of T1,T2 st f = g holds for X being Subset of S1 for Y being Subset of T1 st X = Y holds ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) let f be Function of S1,S2; ::_thesis: for g being Function of T1,T2 st f = g holds for X being Subset of S1 for Y being Subset of T1 st X = Y holds ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) let g be Function of T1,T2; ::_thesis: ( f = g implies for X being Subset of S1 for Y being Subset of T1 st X = Y holds ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) ) assume A3: f = g ; ::_thesis: for X being Subset of S1 for Y being Subset of T1 st X = Y holds ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) let X be Subset of S1; ::_thesis: for Y being Subset of T1 st X = Y holds ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) let Y be Subset of T1; ::_thesis: ( X = Y implies ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) ) assume A4: X = Y ; ::_thesis: ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) thus ( f preserves_sup_of X implies g preserves_sup_of Y ) ::_thesis: ( f preserves_inf_of X implies g preserves_inf_of Y ) proof assume A5: ( ex_sup_of X,S1 implies ( ex_sup_of f .: X,S2 & sup (f .: X) = f . (sup X) ) ) ; :: according to WAYBEL_0:def_31 ::_thesis: g preserves_sup_of Y assume A6: ex_sup_of Y,T1 ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of g .: Y,T2 & sup (g .: Y) = g . (sup Y) ) hence ex_sup_of g .: Y,T2 by A1, A2, A3, A4, A5, YELLOW_0:14; ::_thesis: sup (g .: Y) = g . (sup Y) sup (f .: X) = sup (g .: Y) by A1, A2, A3, A4, A5, A6, YELLOW_0:14, YELLOW_0:26; hence sup (g .: Y) = g . (sup Y) by A1, A3, A4, A5, A6, YELLOW_0:14, YELLOW_0:26; ::_thesis: verum end; assume A7: ( ex_inf_of X,S1 implies ( ex_inf_of f .: X,S2 & inf (f .: X) = f . (inf X) ) ) ; :: according to WAYBEL_0:def_30 ::_thesis: g preserves_inf_of Y assume A8: ex_inf_of Y,T1 ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of g .: Y,T2 & inf (g .: Y) = g . (inf Y) ) hence ex_inf_of g .: Y,T2 by A1, A2, A3, A4, A7, YELLOW_0:14; ::_thesis: inf (g .: Y) = g . (inf Y) inf (f .: X) = inf (g .: Y) by A1, A2, A3, A4, A7, A8, YELLOW_0:14, YELLOW_0:27; hence inf (g .: Y) = g . (inf Y) by A1, A3, A4, A7, A8, YELLOW_0:14, YELLOW_0:27; ::_thesis: verum end; definition let L1, L2 be non empty RelStr ; let f be Function of L1,L2; attrf is infs-preserving means :: WAYBEL_0:def 32 for X being Subset of L1 holds f preserves_inf_of X; attrf is sups-preserving means :: WAYBEL_0:def 33 for X being Subset of L1 holds f preserves_sup_of X; attrf is meet-preserving means :: WAYBEL_0:def 34 for x, y being Element of L1 holds f preserves_inf_of {x,y}; attrf is join-preserving means :: WAYBEL_0:def 35 for x, y being Element of L1 holds f preserves_sup_of {x,y}; attrf is filtered-infs-preserving means :: WAYBEL_0:def 36 for X being Subset of L1 st not X is empty & X is filtered holds f preserves_inf_of X; attrf is directed-sups-preserving means :: WAYBEL_0:def 37 for X being Subset of L1 st not X is empty & X is directed holds f preserves_sup_of X; end; :: deftheorem defines infs-preserving WAYBEL_0:def_32_:_ for L1, L2 being non empty RelStr for f being Function of L1,L2 holds ( f is infs-preserving iff for X being Subset of L1 holds f preserves_inf_of X ); :: deftheorem defines sups-preserving WAYBEL_0:def_33_:_ for L1, L2 being non empty RelStr for f being Function of L1,L2 holds ( f is sups-preserving iff for X being Subset of L1 holds f preserves_sup_of X ); :: deftheorem defines meet-preserving WAYBEL_0:def_34_:_ for L1, L2 being non empty RelStr for f being Function of L1,L2 holds ( f is meet-preserving iff for x, y being Element of L1 holds f preserves_inf_of {x,y} ); :: deftheorem defines join-preserving WAYBEL_0:def_35_:_ for L1, L2 being non empty RelStr for f being Function of L1,L2 holds ( f is join-preserving iff for x, y being Element of L1 holds f preserves_sup_of {x,y} ); :: deftheorem defines filtered-infs-preserving WAYBEL_0:def_36_:_ for L1, L2 being non empty RelStr for f being Function of L1,L2 holds ( f is filtered-infs-preserving iff for X being Subset of L1 st not X is empty & X is filtered holds f preserves_inf_of X ); :: deftheorem defines directed-sups-preserving WAYBEL_0:def_37_:_ for L1, L2 being non empty RelStr for f being Function of L1,L2 holds ( f is directed-sups-preserving iff for X being Subset of L1 st not X is empty & X is directed holds f preserves_sup_of X ); registration let L1, L2 be non empty RelStr ; cluster Function-like V21( the carrier of L1, the carrier of L2) infs-preserving -> meet-preserving filtered-infs-preserving for Element of K10(K11( the carrier of L1, the carrier of L2)); coherence for b1 being Function of L1,L2 st b1 is infs-preserving holds ( b1 is filtered-infs-preserving & b1 is meet-preserving ) proof let f be Function of L1,L2; ::_thesis: ( f is infs-preserving implies ( f is filtered-infs-preserving & f is meet-preserving ) ) assume A1: for X being Subset of L1 holds f preserves_inf_of X ; :: according to WAYBEL_0:def_32 ::_thesis: ( f is filtered-infs-preserving & f is meet-preserving ) hence for X being Subset of L1 st not X is empty & X is filtered holds f preserves_inf_of X ; :: according to WAYBEL_0:def_36 ::_thesis: f is meet-preserving thus for x, y being Element of L1 holds f preserves_inf_of {x,y} by A1; :: according to WAYBEL_0:def_34 ::_thesis: verum end; cluster Function-like V21( the carrier of L1, the carrier of L2) sups-preserving -> join-preserving directed-sups-preserving for Element of K10(K11( the carrier of L1, the carrier of L2)); coherence for b1 being Function of L1,L2 st b1 is sups-preserving holds ( b1 is directed-sups-preserving & b1 is join-preserving ) proof let f be Function of L1,L2; ::_thesis: ( f is sups-preserving implies ( f is directed-sups-preserving & f is join-preserving ) ) assume A2: for X being Subset of L1 holds f preserves_sup_of X ; :: according to WAYBEL_0:def_33 ::_thesis: ( f is directed-sups-preserving & f is join-preserving ) hence for X being Subset of L1 st not X is empty & X is directed holds f preserves_sup_of X ; :: according to WAYBEL_0:def_37 ::_thesis: f is join-preserving thus for x, y being Element of L1 holds f preserves_sup_of {x,y} by A2; :: according to WAYBEL_0:def_35 ::_thesis: verum end; end; definition let S, T be RelStr ; let f be Function of S,T; attrf is isomorphic means :Def38: :: WAYBEL_0:def 38 ( f is one-to-one & f is monotone & ex g being Function of T,S st ( g = f " & g is monotone ) ) if ( not S is empty & not T is empty ) otherwise ( S is empty & T is empty ); correctness consistency verum; ; end; :: deftheorem Def38 defines isomorphic WAYBEL_0:def_38_:_ for S, T being RelStr for f being Function of S,T holds ( ( not S is empty & not T is empty implies ( f is isomorphic iff ( f is one-to-one & f is monotone & ex g being Function of T,S st ( g = f " & g is monotone ) ) ) ) & ( ( S is empty or T is empty ) implies ( f is isomorphic iff ( S is empty & T is empty ) ) ) ); theorem Th66: :: WAYBEL_0:66 for S, T being non empty RelStr for f being Function of S,T holds ( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds ( x <= y iff f . x <= f . y ) ) ) ) proof let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T holds ( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds ( x <= y iff f . x <= f . y ) ) ) ) let f be Function of S,T; ::_thesis: ( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds ( x <= y iff f . x <= f . y ) ) ) ) hereby ::_thesis: ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds ( x <= y iff f . x <= f . y ) ) implies f is isomorphic ) assume A1: f is isomorphic ; ::_thesis: ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) ) ) ) hence f is one-to-one by Def38; ::_thesis: ( rng f = the carrier of T & ( for x, y being Element of S holds ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) ) ) ) consider g being Function of T,S such that A2: g = f " and A3: g is monotone by A1, Def38; A4: ( f is one-to-one & f is monotone ) by A1, Def38; then rng f = dom g by A2, FUNCT_1:33; hence rng f = the carrier of T by FUNCT_2:def_1; ::_thesis: for x, y being Element of S holds ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) ) let x, y be Element of S; ::_thesis: ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) ) thus ( x <= y implies f . x <= f . y ) by A4, ORDERS_3:def_5; ::_thesis: ( f . x <= f . y implies x <= y ) assume A5: f . x <= f . y ; ::_thesis: x <= y A6: g . (f . x) = x by A2, A4, FUNCT_2:26; g . (f . y) = y by A2, A4, FUNCT_2:26; hence x <= y by A3, A5, A6, ORDERS_3:def_5; ::_thesis: verum end; assume that A7: f is one-to-one and A8: rng f = the carrier of T and A9: for x, y being Element of S holds ( x <= y iff f . x <= f . y ) ; ::_thesis: f is isomorphic percases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ; :: according to WAYBEL_0:def_38 case ( not S is empty & not T is empty ) ; ::_thesis: ( f is one-to-one & f is monotone & ex g being Function of T,S st ( g = f " & g is monotone ) ) thus f is one-to-one by A7; ::_thesis: ( f is monotone & ex g being Function of T,S st ( g = f " & g is monotone ) ) thus for x, y being Element of S st x <= y holds for a, b being Element of T st a = f . x & b = f . y holds a <= b by A9; :: according to ORDERS_3:def_5 ::_thesis: ex g being Function of T,S st ( g = f " & g is monotone ) reconsider g = f " as Function of T,S by A7, A8, FUNCT_2:25; take g ; ::_thesis: ( g = f " & g is monotone ) thus g = f " ; ::_thesis: g is monotone let x, y be Element of T; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of S holds ( not b1 = g . x or not b2 = g . y or b1 <= b2 ) ) consider a being set such that A10: a in dom f and A11: x = f . a by A8, FUNCT_1:def_3; consider b being set such that A12: b in dom f and A13: y = f . b by A8, FUNCT_1:def_3; reconsider a = a, b = b as Element of S by A10, A12; A14: g . x = a by A7, A11, FUNCT_2:26; g . y = b by A7, A13, FUNCT_2:26; hence ( not x <= y or for b1, b2 being Element of the carrier of S holds ( not b1 = g . x or not b2 = g . y or b1 <= b2 ) ) by A9, A11, A13, A14; ::_thesis: verum end; case ( S is empty or T is empty ) ; ::_thesis: ( S is empty & T is empty ) hence ( S is empty & T is empty ) ; ::_thesis: verum end; end; end; registration let S, T be non empty RelStr ; cluster Function-like V21( the carrier of S, the carrier of T) isomorphic -> one-to-one monotone for Element of K10(K11( the carrier of S, the carrier of T)); coherence for b1 being Function of S,T st b1 is isomorphic holds ( b1 is one-to-one & b1 is monotone ) by Def38; end; theorem :: WAYBEL_0:67 for S, T being non empty RelStr for f being Function of S,T st f is isomorphic holds ( f " is Function of T,S & rng (f ") = the carrier of S ) proof let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T st f is isomorphic holds ( f " is Function of T,S & rng (f ") = the carrier of S ) let f be Function of S,T; ::_thesis: ( f is isomorphic implies ( f " is Function of T,S & rng (f ") = the carrier of S ) ) assume A1: f is isomorphic ; ::_thesis: ( f " is Function of T,S & rng (f ") = the carrier of S ) then A2: rng f = the carrier of T by Th66; A3: dom f = the carrier of S by FUNCT_2:def_1; A4: dom (f ") = the carrier of T by A1, A2, FUNCT_1:33; rng (f ") = the carrier of S by A1, A3, FUNCT_1:33; hence ( f " is Function of T,S & rng (f ") = the carrier of S ) by A4, FUNCT_2:1; ::_thesis: verum end; theorem :: WAYBEL_0:68 for S, T being non empty RelStr for f being Function of S,T st f is isomorphic holds for g being Function of T,S st g = f " holds g is isomorphic proof let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T st f is isomorphic holds for g being Function of T,S st g = f " holds g is isomorphic let f be Function of S,T; ::_thesis: ( f is isomorphic implies for g being Function of T,S st g = f " holds g is isomorphic ) assume A1: f is isomorphic ; ::_thesis: for g being Function of T,S st g = f " holds g is isomorphic then A2: ex h being Function of T,S st ( h = f " & h is monotone ) by Def38; let g be Function of T,S; ::_thesis: ( g = f " implies g is isomorphic ) assume A3: g = f " ; ::_thesis: g is isomorphic percases ( ( not T is empty & not S is empty ) or T is empty or S is empty ) ; :: according to WAYBEL_0:def_38 case ( not T is empty & not S is empty ) ; ::_thesis: ( g is one-to-one & g is monotone & ex g being Function of S,T st ( g = g " & g is monotone ) ) thus ( g is one-to-one & g is monotone ) by A1, A2, A3, FUNCT_1:40; ::_thesis: ex g being Function of S,T st ( g = g " & g is monotone ) (f ") " = f by A1, FUNCT_1:43; hence ex g being Function of S,T st ( g = g " & g is monotone ) by A1, A3; ::_thesis: verum end; case ( T is empty or S is empty ) ; ::_thesis: ( T is empty & S is empty ) hence ( T is empty & S is empty ) ; ::_thesis: verum end; end; end; theorem Th69: :: WAYBEL_0:69 for S, T being non empty Poset for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds f is monotone proof let S, T be non empty Poset; ::_thesis: for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds f is monotone let f be Function of S,T; ::_thesis: ( ( for X being Filter of S holds f preserves_inf_of X ) implies f is monotone ) assume A1: for X being Filter of S holds f preserves_inf_of X ; ::_thesis: f is monotone let x, y be Element of S; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) ) A2: ex_inf_of {x},S by YELLOW_0:38; A3: ex_inf_of {y},S by YELLOW_0:38; A4: f preserves_inf_of uparrow x by A1; A5: f preserves_inf_of uparrow y by A1; A6: ex_inf_of uparrow x,S by A2, Th37; A7: ex_inf_of uparrow y,S by A3, Th37; A8: ex_inf_of f .: (uparrow x),T by A4, A6, Def30; A9: ex_inf_of f .: (uparrow y),T by A5, A7, Def30; A10: inf (f .: (uparrow x)) = f . (inf (uparrow x)) by A4, A6, Def30; A11: inf (f .: (uparrow y)) = f . (inf (uparrow y)) by A5, A7, Def30; assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) then A12: uparrow y c= uparrow x by Th22; A13: inf (f .: (uparrow x)) = f . (inf {x}) by A10, Th38, YELLOW_0:38; A14: inf (f .: (uparrow y)) = f . (inf {y}) by A11, Th38, YELLOW_0:38; A15: inf (f .: (uparrow x)) = f . x by A13, YELLOW_0:39; inf (f .: (uparrow y)) = f . y by A14, YELLOW_0:39; hence for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) by A8, A9, A12, A15, RELAT_1:123, YELLOW_0:35; ::_thesis: verum end; theorem :: WAYBEL_0:70 for S, T being non empty Poset for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds f is filtered-infs-preserving proof let S, T be non empty Poset; ::_thesis: for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds f is filtered-infs-preserving let f be Function of S,T; ::_thesis: ( ( for X being Filter of S holds f preserves_inf_of X ) implies f is filtered-infs-preserving ) assume A1: for X being Filter of S holds f preserves_inf_of X ; ::_thesis: f is filtered-infs-preserving let X be Subset of S; :: according to WAYBEL_0:def_36 ::_thesis: ( not X is empty & X is filtered implies f preserves_inf_of X ) assume that A2: ( not X is empty & X is filtered ) and A3: ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) reconsider Y = X as non empty filtered Subset of S by A2; uparrow Y is Filter of S ; then A4: f preserves_inf_of uparrow X by A1; A5: ex_inf_of uparrow X,S by A3, Th37; then A6: ex_inf_of f .: (uparrow X),T by A4, Def30; A7: inf (f .: (uparrow X)) = f . (inf (uparrow X)) by A4, A5, Def30; A8: inf (uparrow X) = inf X by A3, Th38; A9: f .: X c= f .: (uparrow X) by Th16, RELAT_1:123; A10: f .: (uparrow X) is_>=_than f . (inf X) by A6, A7, A8, YELLOW_0:31; A11: f .: X is_>=_than f . (inf X) proof let x be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not x in f .: X or f . (inf X) <= x ) assume x in f .: X ; ::_thesis: f . (inf X) <= x hence f . (inf X) <= x by A9, A10, LATTICE3:def_8; ::_thesis: verum end; A12: now__::_thesis:_for_b_being_Element_of_T_st_f_.:_X_is_>=_than_b_holds_ f_._(inf_X)_>=_b let b be Element of T; ::_thesis: ( f .: X is_>=_than b implies f . (inf X) >= b ) assume A13: f .: X is_>=_than b ; ::_thesis: f . (inf X) >= b f .: (uparrow X) is_>=_than b proof let a be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not a in f .: (uparrow X) or b <= a ) assume a in f .: (uparrow X) ; ::_thesis: b <= a then consider x being set such that x in dom f and A14: x in uparrow X and A15: a = f . x by FUNCT_1:def_6; uparrow X = { z where z is Element of S : ex y being Element of S st ( z >= y & y in X ) } by Th15; then consider z being Element of S such that A16: x = z and A17: ex y being Element of S st ( z >= y & y in X ) by A14; consider y being Element of S such that A18: z >= y and A19: y in X by A17; A20: f is monotone by A1, Th69; A21: f . y in f .: X by A19, FUNCT_2:35; A22: f . z >= f . y by A18, A20, ORDERS_3:def_5; f . y >= b by A13, A21, LATTICE3:def_8; hence b <= a by A15, A16, A22, ORDERS_2:3; ::_thesis: verum end; hence f . (inf X) >= b by A6, A7, A8, YELLOW_0:31; ::_thesis: verum end; hence ex_inf_of f .: X,T by A11, YELLOW_0:16; ::_thesis: inf (f .: X) = f . (inf X) hence inf (f .: X) = f . (inf X) by A11, A12, YELLOW_0:def_10; ::_thesis: verum end; theorem :: WAYBEL_0:71 for S being Semilattice for T being non empty Poset for f being Function of S,T st ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds f is infs-preserving proof let S be Semilattice; ::_thesis: for T being non empty Poset for f being Function of S,T st ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds f is infs-preserving let T be non empty Poset; ::_thesis: for f being Function of S,T st ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds f is infs-preserving let f be Function of S,T; ::_thesis: ( ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) implies f is infs-preserving ) assume that A1: for X being finite Subset of S holds f preserves_inf_of X and A2: for X being non empty filtered Subset of S holds f preserves_inf_of X ; ::_thesis: f is infs-preserving let X be Subset of S; :: according to WAYBEL_0:def_32 ::_thesis: f preserves_inf_of X assume A3: ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) defpred S1[ set ] means ex Y being finite Subset of X st ( ex_inf_of Y,S & $1 = "/\" (Y,S) ); consider Z being set such that A4: for x being set holds ( x in Z iff ( x in the carrier of S & S1[x] ) ) from XBOOLE_0:sch_1(); Z c= the carrier of S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in the carrier of S ) thus ( not x in Z or x in the carrier of S ) by A4; ::_thesis: verum end; then reconsider Z = Z as Subset of S ; A5: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ ex_inf_of_Y,S let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_inf_of Y,S ) Y is Subset of S by XBOOLE_1:1; hence ( Y <> {} implies ex_inf_of Y,S ) by YELLOW_0:55; ::_thesis: verum end; A6: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ "/\"_(Y,S)_in_Z let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "/\" (Y,S) in Z ) reconsider Y9 = Y as Subset of S by XBOOLE_1:1; assume Y <> {} ; ::_thesis: "/\" (Y,S) in Z then ex_inf_of Y9,S by YELLOW_0:55; hence "/\" (Y,S) in Z by A4; ::_thesis: verum end; A7: for x being Element of S st x in Z holds ex Y being finite Subset of X st ( ex_inf_of Y,S & x = "/\" (Y,S) ) by A4; then A8: Z is filtered by A5, A6, Th56; A9: ex_inf_of Z,S by A3, A5, A6, A7, Th58; ( Z = {} or Z <> {} ) ; then A10: f preserves_inf_of Z by A1, A2, A8; then A11: ex_inf_of f .: Z,T by A9, Def30; A12: inf (f .: Z) = f . (inf Z) by A9, A10, Def30; A13: inf Z = inf X by A3, A5, A6, A7, Th59; X c= Z proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Z ) assume A14: x in X ; ::_thesis: x in Z then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31; reconsider x = x as Element of S by A14; Y is Subset of S by XBOOLE_1:1; then A15: ex_inf_of Y,S by YELLOW_0:55; x = "/\" (Y,S) by YELLOW_0:39; hence x in Z by A4, A15; ::_thesis: verum end; then A16: f .: X c= f .: Z by RELAT_1:123; A17: f .: Z is_>=_than f . (inf X) by A11, A12, A13, YELLOW_0:31; A18: f .: X is_>=_than f . (inf X) proof let x be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not x in f .: X or f . (inf X) <= x ) assume x in f .: X ; ::_thesis: f . (inf X) <= x hence f . (inf X) <= x by A16, A17, LATTICE3:def_8; ::_thesis: verum end; A19: now__::_thesis:_for_b_being_Element_of_T_st_f_.:_X_is_>=_than_b_holds_ f_._(inf_X)_>=_b let b be Element of T; ::_thesis: ( f .: X is_>=_than b implies f . (inf X) >= b ) assume A20: f .: X is_>=_than b ; ::_thesis: f . (inf X) >= b f .: Z is_>=_than b proof let a be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not a in f .: Z or b <= a ) assume a in f .: Z ; ::_thesis: b <= a then consider x being set such that x in dom f and A21: x in Z and A22: a = f . x by FUNCT_1:def_6; consider Y being finite Subset of X such that A23: ex_inf_of Y,S and A24: x = "/\" (Y,S) by A4, A21; reconsider Y = Y as Subset of S by XBOOLE_1:1; A25: f .: Y c= f .: X by RELAT_1:123; A26: f preserves_inf_of Y by A1; A27: b is_<=_than f .: Y by A20, A25, YELLOW_0:9; A28: a = "/\" ((f .: Y),T) by A22, A23, A24, A26, Def30; ex_inf_of f .: Y,T by A23, A26, Def30; hence b <= a by A27, A28, YELLOW_0:def_10; ::_thesis: verum end; hence f . (inf X) >= b by A11, A12, A13, YELLOW_0:31; ::_thesis: verum end; hence ex_inf_of f .: X,T by A18, YELLOW_0:16; ::_thesis: inf (f .: X) = f . (inf X) hence inf (f .: X) = f . (inf X) by A18, A19, YELLOW_0:def_10; ::_thesis: verum end; theorem Th72: :: WAYBEL_0:72 for S, T being non empty Poset for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds f is monotone proof let S, T be non empty Poset; ::_thesis: for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds f is monotone let f be Function of S,T; ::_thesis: ( ( for X being Ideal of S holds f preserves_sup_of X ) implies f is monotone ) assume A1: for X being Ideal of S holds f preserves_sup_of X ; ::_thesis: f is monotone let x, y be Element of S; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) ) A2: ex_sup_of {x},S by YELLOW_0:38; A3: ex_sup_of {y},S by YELLOW_0:38; A4: f preserves_sup_of downarrow x by A1; A5: f preserves_sup_of downarrow y by A1; A6: ex_sup_of downarrow x,S by A2, Th32; A7: ex_sup_of downarrow y,S by A3, Th32; A8: ex_sup_of f .: (downarrow x),T by A4, A6, Def31; A9: ex_sup_of f .: (downarrow y),T by A5, A7, Def31; A10: sup (f .: (downarrow x)) = f . (sup (downarrow x)) by A4, A6, Def31; A11: sup (f .: (downarrow y)) = f . (sup (downarrow y)) by A5, A7, Def31; assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) then A12: downarrow x c= downarrow y by Th21; A13: sup (f .: (downarrow x)) = f . (sup {x}) by A10, Th33, YELLOW_0:38; A14: sup (f .: (downarrow y)) = f . (sup {y}) by A11, Th33, YELLOW_0:38; A15: sup (f .: (downarrow x)) = f . x by A13, YELLOW_0:39; sup (f .: (downarrow y)) = f . y by A14, YELLOW_0:39; hence for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) by A8, A9, A12, A15, RELAT_1:123, YELLOW_0:34; ::_thesis: verum end; theorem :: WAYBEL_0:73 for S, T being non empty Poset for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds f is directed-sups-preserving proof let S, T be non empty Poset; ::_thesis: for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds f is directed-sups-preserving let f be Function of S,T; ::_thesis: ( ( for X being Ideal of S holds f preserves_sup_of X ) implies f is directed-sups-preserving ) assume A1: for X being Ideal of S holds f preserves_sup_of X ; ::_thesis: f is directed-sups-preserving let X be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( not X is empty & X is directed implies f preserves_sup_of X ) assume that A2: ( not X is empty & X is directed ) and A3: ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) ) reconsider Y = X as non empty directed Subset of S by A2; downarrow Y is Ideal of S ; then A4: f preserves_sup_of downarrow X by A1; A5: ex_sup_of downarrow X,S by A3, Th32; then A6: ex_sup_of f .: (downarrow X),T by A4, Def31; A7: sup (f .: (downarrow X)) = f . (sup (downarrow X)) by A4, A5, Def31; A8: sup (downarrow X) = sup X by A3, Th33; A9: f .: X c= f .: (downarrow X) by Th16, RELAT_1:123; A10: f .: (downarrow X) is_<=_than f . (sup X) by A6, A7, A8, YELLOW_0:30; A11: f .: X is_<=_than f . (sup X) proof let x be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not x in f .: X or x <= f . (sup X) ) assume x in f .: X ; ::_thesis: x <= f . (sup X) hence x <= f . (sup X) by A9, A10, LATTICE3:def_9; ::_thesis: verum end; A12: now__::_thesis:_for_b_being_Element_of_T_st_f_.:_X_is_<=_than_b_holds_ f_._(sup_X)_<=_b let b be Element of T; ::_thesis: ( f .: X is_<=_than b implies f . (sup X) <= b ) assume A13: f .: X is_<=_than b ; ::_thesis: f . (sup X) <= b f .: (downarrow X) is_<=_than b proof let a be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not a in f .: (downarrow X) or a <= b ) assume a in f .: (downarrow X) ; ::_thesis: a <= b then consider x being set such that x in dom f and A14: x in downarrow X and A15: a = f . x by FUNCT_1:def_6; downarrow X = { z where z is Element of S : ex y being Element of S st ( z <= y & y in X ) } by Th14; then consider z being Element of S such that A16: x = z and A17: ex y being Element of S st ( z <= y & y in X ) by A14; consider y being Element of S such that A18: z <= y and A19: y in X by A17; A20: f is monotone by A1, Th72; A21: f . y in f .: X by A19, FUNCT_2:35; A22: f . z <= f . y by A18, A20, ORDERS_3:def_5; f . y <= b by A13, A21, LATTICE3:def_9; hence a <= b by A15, A16, A22, ORDERS_2:3; ::_thesis: verum end; hence f . (sup X) <= b by A6, A7, A8, YELLOW_0:30; ::_thesis: verum end; hence ex_sup_of f .: X,T by A11, YELLOW_0:15; ::_thesis: sup (f .: X) = f . (sup X) hence sup (f .: X) = f . (sup X) by A11, A12, YELLOW_0:def_9; ::_thesis: verum end; theorem :: WAYBEL_0:74 for S being sup-Semilattice for T being non empty Poset for f being Function of S,T st ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) holds f is sups-preserving proof let S be sup-Semilattice; ::_thesis: for T being non empty Poset for f being Function of S,T st ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) holds f is sups-preserving let T be non empty Poset; ::_thesis: for f being Function of S,T st ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) holds f is sups-preserving let f be Function of S,T; ::_thesis: ( ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) implies f is sups-preserving ) assume that A1: for X being finite Subset of S holds f preserves_sup_of X and A2: for X being non empty directed Subset of S holds f preserves_sup_of X ; ::_thesis: f is sups-preserving let X be Subset of S; :: according to WAYBEL_0:def_33 ::_thesis: f preserves_sup_of X assume A3: ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) ) defpred S1[ set ] means ex Y being finite Subset of X st ( ex_sup_of Y,S & $1 = "\/" (Y,S) ); consider Z being set such that A4: for x being set holds ( x in Z iff ( x in the carrier of S & S1[x] ) ) from XBOOLE_0:sch_1(); Z c= the carrier of S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in the carrier of S ) thus ( not x in Z or x in the carrier of S ) by A4; ::_thesis: verum end; then reconsider Z = Z as Subset of S ; A5: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ ex_sup_of_Y,S let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_sup_of Y,S ) Y is Subset of S by XBOOLE_1:1; hence ( Y <> {} implies ex_sup_of Y,S ) by YELLOW_0:54; ::_thesis: verum end; A6: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_ "\/"_(Y,S)_in_Z let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "\/" (Y,S) in Z ) reconsider Y9 = Y as Subset of S by XBOOLE_1:1; assume Y <> {} ; ::_thesis: "\/" (Y,S) in Z then ex_sup_of Y9,S by YELLOW_0:54; hence "\/" (Y,S) in Z by A4; ::_thesis: verum end; A7: for x being Element of S st x in Z holds ex Y being finite Subset of X st ( ex_sup_of Y,S & x = "\/" (Y,S) ) by A4; then A8: Z is directed by A5, A6, Th51; A9: ex_sup_of Z,S by A3, A5, A6, A7, Th53; ( Z = {} or Z <> {} ) ; then A10: f preserves_sup_of Z by A1, A2, A8; then A11: ex_sup_of f .: Z,T by A9, Def31; A12: sup (f .: Z) = f . (sup Z) by A9, A10, Def31; A13: sup Z = sup X by A3, A5, A6, A7, Th54; X c= Z proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Z ) assume A14: x in X ; ::_thesis: x in Z then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31; reconsider x = x as Element of S by A14; Y is Subset of S by XBOOLE_1:1; then A15: ex_sup_of Y,S by YELLOW_0:54; x = "\/" (Y,S) by YELLOW_0:39; hence x in Z by A4, A15; ::_thesis: verum end; then A16: f .: X c= f .: Z by RELAT_1:123; A17: f .: Z is_<=_than f . (sup X) by A11, A12, A13, YELLOW_0:30; A18: f .: X is_<=_than f . (sup X) proof let x be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not x in f .: X or x <= f . (sup X) ) assume x in f .: X ; ::_thesis: x <= f . (sup X) hence x <= f . (sup X) by A16, A17, LATTICE3:def_9; ::_thesis: verum end; A19: now__::_thesis:_for_b_being_Element_of_T_st_f_.:_X_is_<=_than_b_holds_ f_._(sup_X)_<=_b let b be Element of T; ::_thesis: ( f .: X is_<=_than b implies f . (sup X) <= b ) assume A20: f .: X is_<=_than b ; ::_thesis: f . (sup X) <= b f .: Z is_<=_than b proof let a be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not a in f .: Z or a <= b ) assume a in f .: Z ; ::_thesis: a <= b then consider x being set such that x in dom f and A21: x in Z and A22: a = f . x by FUNCT_1:def_6; consider Y being finite Subset of X such that A23: ex_sup_of Y,S and A24: x = "\/" (Y,S) by A4, A21; reconsider Y = Y as Subset of S by XBOOLE_1:1; A25: f .: Y c= f .: X by RELAT_1:123; A26: f preserves_sup_of Y by A1; A27: b is_>=_than f .: Y by A20, A25, YELLOW_0:9; A28: a = "\/" ((f .: Y),T) by A22, A23, A24, A26, Def31; ex_sup_of f .: Y,T by A23, A26, Def31; hence a <= b by A27, A28, YELLOW_0:def_9; ::_thesis: verum end; hence f . (sup X) <= b by A11, A12, A13, YELLOW_0:30; ::_thesis: verum end; hence ex_sup_of f .: X,T by A18, YELLOW_0:15; ::_thesis: sup (f .: X) = f . (sup X) hence sup (f .: X) = f . (sup X) by A18, A19, YELLOW_0:def_9; ::_thesis: verum end; begin definition let L be non empty reflexive RelStr ; attrL is up-complete means :Def39: :: WAYBEL_0:def 39 for X being non empty directed Subset of L ex x being Element of L st ( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds x <= y ) ); end; :: deftheorem Def39 defines up-complete WAYBEL_0:def_39_:_ for L being non empty reflexive RelStr holds ( L is up-complete iff for X being non empty directed Subset of L ex x being Element of L st ( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds x <= y ) ) ); registration cluster reflexive with_suprema up-complete -> reflexive with_suprema upper-bounded for RelStr ; coherence for b1 being reflexive with_suprema RelStr st b1 is up-complete holds b1 is upper-bounded proof let L be reflexive with_suprema RelStr ; ::_thesis: ( L is up-complete implies L is upper-bounded ) assume A1: L is up-complete ; ::_thesis: L is upper-bounded [#] L = the carrier of L ; then ex x being Element of L st ( x is_>=_than the carrier of L & ( for y being Element of L st y is_>=_than the carrier of L holds x <= y ) ) by A1, Def39; hence ex x being Element of L st x is_>=_than the carrier of L ; :: according to YELLOW_0:def_5 ::_thesis: verum end; end; theorem :: WAYBEL_0:75 for L being non empty reflexive antisymmetric RelStr holds ( L is up-complete iff for X being non empty directed Subset of L holds ex_sup_of X,L ) proof let L be non empty reflexive antisymmetric RelStr ; ::_thesis: ( L is up-complete iff for X being non empty directed Subset of L holds ex_sup_of X,L ) hereby ::_thesis: ( ( for X being non empty directed Subset of L holds ex_sup_of X,L ) implies L is up-complete ) assume A1: L is up-complete ; ::_thesis: for X being non empty directed Subset of L holds ex_sup_of X,L let X be non empty directed Subset of L; ::_thesis: ex_sup_of X,L consider x being Element of L such that A2: x is_>=_than X and A3: for y being Element of L st y is_>=_than X holds x <= y by A1, Def39; thus ex_sup_of X,L ::_thesis: verum proof take x ; :: according to YELLOW_0:def_7 ::_thesis: ( X is_<=_than x & ( for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or x <= b1 ) ) & ( for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or ex b2 being Element of the carrier of L st ( X is_<=_than b2 & not b1 <= b2 ) or b1 = x ) ) ) thus ( X is_<=_than x & ( for b being Element of L st X is_<=_than b holds b >= x ) ) by A2, A3; ::_thesis: for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or ex b2 being Element of the carrier of L st ( X is_<=_than b2 & not b1 <= b2 ) or b1 = x ) let c be Element of L; ::_thesis: ( not X is_<=_than c or ex b1 being Element of the carrier of L st ( X is_<=_than b1 & not c <= b1 ) or c = x ) assume that A4: X is_<=_than c and A5: for b being Element of L st X is_<=_than b holds b >= c ; ::_thesis: c = x A6: c <= x by A2, A5; c >= x by A3, A4; hence c = x by A6, ORDERS_2:2; ::_thesis: verum end; end; assume A7: for X being non empty directed Subset of L holds ex_sup_of X,L ; ::_thesis: L is up-complete let X be non empty directed Subset of L; :: according to WAYBEL_0:def_39 ::_thesis: ex x being Element of L st ( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds x <= y ) ) ex_sup_of X,L by A7; then ex a being Element of L st ( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds b >= a ) & ( for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) holds c = a ) ) by YELLOW_0:def_7; hence ex x being Element of L st ( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds x <= y ) ) ; ::_thesis: verum end; definition let L be non empty reflexive RelStr ; attrL is /\-complete means :Def40: :: WAYBEL_0:def 40 for X being non empty Subset of L ex x being Element of L st ( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds x >= y ) ); end; :: deftheorem Def40 defines /\-complete WAYBEL_0:def_40_:_ for L being non empty reflexive RelStr holds ( L is /\-complete iff for X being non empty Subset of L ex x being Element of L st ( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds x >= y ) ) ); theorem Th76: :: WAYBEL_0:76 for L being non empty reflexive antisymmetric RelStr holds ( L is /\-complete iff for X being non empty Subset of L holds ex_inf_of X,L ) proof let L be non empty reflexive antisymmetric RelStr ; ::_thesis: ( L is /\-complete iff for X being non empty Subset of L holds ex_inf_of X,L ) hereby ::_thesis: ( ( for X being non empty Subset of L holds ex_inf_of X,L ) implies L is /\-complete ) assume A1: L is /\-complete ; ::_thesis: for X being non empty Subset of L holds ex_inf_of X,L let X be non empty Subset of L; ::_thesis: ex_inf_of X,L consider x being Element of L such that A2: x is_<=_than X and A3: for y being Element of L st y is_<=_than X holds x >= y by A1, Def40; thus ex_inf_of X,L ::_thesis: verum proof take x ; :: according to YELLOW_0:def_8 ::_thesis: ( x is_<=_than X & ( for b1 being Element of the carrier of L holds ( not b1 is_<=_than X or b1 <= x ) ) & ( for b1 being Element of the carrier of L holds ( not b1 is_<=_than X or ex b2 being Element of the carrier of L st ( b2 is_<=_than X & not b2 <= b1 ) or b1 = x ) ) ) thus ( X is_>=_than x & ( for b being Element of L st X is_>=_than b holds b <= x ) ) by A2, A3; ::_thesis: for b1 being Element of the carrier of L holds ( not b1 is_<=_than X or ex b2 being Element of the carrier of L st ( b2 is_<=_than X & not b2 <= b1 ) or b1 = x ) let c be Element of L; ::_thesis: ( not c is_<=_than X or ex b1 being Element of the carrier of L st ( b1 is_<=_than X & not b1 <= c ) or c = x ) assume that A4: X is_>=_than c and A5: for b being Element of L st X is_>=_than b holds b <= c ; ::_thesis: c = x A6: c <= x by A3, A4; c >= x by A2, A5; hence c = x by A6, ORDERS_2:2; ::_thesis: verum end; end; assume A7: for X being non empty Subset of L holds ex_inf_of X,L ; ::_thesis: L is /\-complete let X be non empty Subset of L; :: according to WAYBEL_0:def_40 ::_thesis: ex x being Element of L st ( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds x >= y ) ) ex_inf_of X,L by A7; then ex a being Element of L st ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds b <= c ) holds c = a ) ) by YELLOW_0:def_8; hence ex x being Element of L st ( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds x >= y ) ) ; ::_thesis: verum end; registration cluster non empty reflexive complete -> non empty reflexive up-complete /\-complete for RelStr ; coherence for b1 being non empty reflexive RelStr st b1 is complete holds ( b1 is up-complete & b1 is /\-complete ) proof let L be non empty reflexive RelStr ; ::_thesis: ( L is complete implies ( L is up-complete & L is /\-complete ) ) assume A1: L is complete ; ::_thesis: ( L is up-complete & L is /\-complete ) thus L is up-complete ::_thesis: L is /\-complete proof let X be non empty directed Subset of L; :: according to WAYBEL_0:def_39 ::_thesis: ex x being Element of L st ( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds x <= y ) ) thus ex x being Element of L st ( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds x <= y ) ) by A1, LATTICE3:def_12; ::_thesis: verum end; let X be non empty Subset of L; :: according to WAYBEL_0:def_40 ::_thesis: ex x being Element of L st ( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds x >= y ) ) set Y = { y where y is Element of L : y is_<=_than X } ; consider x being Element of L such that A2: { y where y is Element of L : y is_<=_than X } is_<=_than x and A3: for b being Element of L st { y where y is Element of L : y is_<=_than X } is_<=_than b holds x <= b by A1, LATTICE3:def_12; take x ; ::_thesis: ( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds x >= y ) ) thus x is_<=_than X ::_thesis: for y being Element of L st y is_<=_than X holds x >= y proof let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in X or x <= y ) assume A4: y in X ; ::_thesis: x <= y y is_>=_than { y where y is Element of L : y is_<=_than X } proof let z be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not z in { y where y is Element of L : y is_<=_than X } or z <= y ) assume z in { y where y is Element of L : y is_<=_than X } ; ::_thesis: z <= y then ex a being Element of L st ( z = a & a is_<=_than X ) ; hence z <= y by A4, LATTICE3:def_8; ::_thesis: verum end; hence x <= y by A3; ::_thesis: verum end; let y be Element of L; ::_thesis: ( y is_<=_than X implies x >= y ) assume y is_<=_than X ; ::_thesis: x >= y then y in { y where y is Element of L : y is_<=_than X } ; hence x >= y by A2, LATTICE3:def_9; ::_thesis: verum end; cluster non empty reflexive /\-complete -> non empty reflexive lower-bounded for RelStr ; coherence for b1 being non empty reflexive RelStr st b1 is /\-complete holds b1 is lower-bounded proof let L be non empty reflexive RelStr ; ::_thesis: ( L is /\-complete implies L is lower-bounded ) assume L is /\-complete ; ::_thesis: L is lower-bounded then ex x being Element of L st ( x is_<=_than [#] L & ( for y being Element of L st y is_<=_than [#] L holds x >= y ) ) by Def40; hence ex x being Element of L st x is_<=_than the carrier of L ; :: according to YELLOW_0:def_4 ::_thesis: verum end; cluster non empty reflexive transitive antisymmetric with_suprema lower-bounded up-complete -> non empty complete for RelStr ; coherence for b1 being non empty Poset st b1 is up-complete & b1 is with_suprema & b1 is lower-bounded holds b1 is complete proof let L be non empty Poset; ::_thesis: ( L is up-complete & L is with_suprema & L is lower-bounded implies L is complete ) assume A5: ( L is up-complete & L is with_suprema & L is lower-bounded ) ; ::_thesis: L is complete then reconsider K = L as non empty with_suprema lower-bounded Poset ; let X be set ; :: according to LATTICE3:def_12 ::_thesis: ex b1 being Element of the carrier of L st ( X is_<=_than b1 & ( for b2 being Element of the carrier of L holds ( not X is_<=_than b2 or b1 <= b2 ) ) ) reconsider X9 = X /\ the carrier of L as Subset of L by XBOOLE_1:17; reconsider A = X9 as Subset of K ; A6: now__::_thesis:_for_Y_being_finite_Subset_of_X9_st_Y_<>_{}_holds_ ex_sup_of_Y,L let Y be finite Subset of X9; ::_thesis: ( Y <> {} implies ex_sup_of Y,L ) Y c= the carrier of L by XBOOLE_1:1; hence ( Y <> {} implies ex_sup_of Y,L ) by A5, YELLOW_0:54; ::_thesis: verum end; A7: now__::_thesis:_for_x_being_Element_of_L_st_x_in_finsups_X9_holds_ ex_Y_being_finite_Subset_of_X9_st_ (_ex_sup_of_Y,L_&_x_=_"\/"_(Y,L)_) let x be Element of L; ::_thesis: ( x in finsups X9 implies ex Y being finite Subset of X9 st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ) assume x in finsups X9 ; ::_thesis: ex Y being finite Subset of X9 st ( ex_sup_of Y,L & x = "\/" (Y,L) ) then ex Y being finite Subset of X9 st ( x = "\/" (Y,L) & ex_sup_of Y,L ) ; hence ex Y being finite Subset of X9 st ( ex_sup_of Y,L & x = "\/" (Y,L) ) ; ::_thesis: verum end; A8: now__::_thesis:_for_Y_being_finite_Subset_of_X9_st_Y_<>_{}_holds_ "\/"_(Y,L)_in_finsups_X9 let Y be finite Subset of X9; ::_thesis: ( Y <> {} implies "\/" (Y,L) in finsups X9 ) reconsider Z = Y as Subset of L by XBOOLE_1:1; assume Y <> {} ; ::_thesis: "\/" (Y,L) in finsups X9 then ex_sup_of Z,L by A5, YELLOW_0:54; hence "\/" (Y,L) in finsups X9 ; ::_thesis: verum end; reconsider fX = finsups A as non empty directed Subset of L ; consider x being Element of L such that A9: fX is_<=_than x and A10: for y being Element of L st fX is_<=_than y holds x <= y by A5, Def39; take x ; ::_thesis: ( X is_<=_than x & ( for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or x <= b1 ) ) ) X9 is_<=_than x by A6, A7, A8, A9, Th52; hence X is_<=_than x by YELLOW_0:5; ::_thesis: for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or x <= b1 ) let y be Element of L; ::_thesis: ( not X is_<=_than y or x <= y ) assume y is_>=_than X ; ::_thesis: x <= y then y is_>=_than X9 by YELLOW_0:5; then y is_>=_than fX by A6, A7, A8, Th52; hence x <= y by A10; ::_thesis: verum end; end; registration cluster non empty reflexive antisymmetric /\-complete -> non empty reflexive antisymmetric with_infima for RelStr ; coherence for b1 being non empty reflexive antisymmetric RelStr st b1 is /\-complete holds b1 is with_infima proof let L be non empty reflexive antisymmetric RelStr ; ::_thesis: ( L is /\-complete implies L is with_infima ) assume L is /\-complete ; ::_thesis: L is with_infima then for a, b being Element of L holds ex_inf_of {a,b},L by Th76; hence L is with_infima by YELLOW_0:21; ::_thesis: verum end; end; registration cluster non empty reflexive antisymmetric upper-bounded /\-complete -> non empty reflexive antisymmetric with_suprema upper-bounded for RelStr ; coherence for b1 being non empty reflexive antisymmetric upper-bounded RelStr st b1 is /\-complete holds b1 is with_suprema proof let L be non empty reflexive antisymmetric upper-bounded RelStr ; ::_thesis: ( L is /\-complete implies L is with_suprema ) assume A1: L is /\-complete ; ::_thesis: L is with_suprema now__::_thesis:_for_a,_b_being_Element_of_L_holds_ex_sup_of_{a,b},L let a, b be Element of L; ::_thesis: ex_sup_of {a,b},L set X = { x where x is Element of L : ( x >= a & x >= b ) } ; { x where x is Element of L : ( x >= a & x >= b ) } c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of L : ( x >= a & x >= b ) } or x in the carrier of L ) assume x in { x where x is Element of L : ( x >= a & x >= b ) } ; ::_thesis: x in the carrier of L then ex z being Element of L st ( x = z & z >= a & z >= b ) ; hence x in the carrier of L ; ::_thesis: verum end; then reconsider X = { x where x is Element of L : ( x >= a & x >= b ) } as Subset of L ; A2: Top L >= a by YELLOW_0:45; Top L >= b by YELLOW_0:45; then Top L in X by A2; then ex_inf_of X,L by A1, Th76; then consider c being Element of L such that A3: c is_<=_than X and A4: for d being Element of L st d is_<=_than X holds d <= c and for e being Element of L st e is_<=_than X & ( for d being Element of L st d is_<=_than X holds d <= e ) holds e = c by YELLOW_0:def_8; A5: c is_>=_than {a,b} proof let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in {a,b} or x <= c ) assume A6: x in {a,b} ; ::_thesis: x <= c x is_<=_than X proof let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in X or x <= y ) assume y in X ; ::_thesis: x <= y then ex z being Element of L st ( y = z & z >= a & z >= b ) ; hence x <= y by A6, TARSKI:def_2; ::_thesis: verum end; hence x <= c by A4; ::_thesis: verum end; now__::_thesis:_for_y_being_Element_of_L_st_y_is_>=_than_{a,b}_holds_ c_<=_y let y be Element of L; ::_thesis: ( y is_>=_than {a,b} implies c <= y ) assume A7: y is_>=_than {a,b} ; ::_thesis: c <= y then A8: y >= a by YELLOW_0:8; y >= b by A7, YELLOW_0:8; then y in X by A8; hence c <= y by A3, LATTICE3:def_8; ::_thesis: verum end; hence ex_sup_of {a,b},L by A5, YELLOW_0:15; ::_thesis: verum end; hence L is with_suprema by YELLOW_0:20; ::_thesis: verum end; end; registration cluster non empty strict V58() reflexive transitive antisymmetric with_suprema with_infima complete for RelStr ; existence ex b1 being LATTICE st ( b1 is complete & b1 is strict ) proof set L = the strict complete LATTICE; take the strict complete LATTICE ; ::_thesis: ( the strict complete LATTICE is complete & the strict complete LATTICE is strict ) thus ( the strict complete LATTICE is complete & the strict complete LATTICE is strict ) ; ::_thesis: verum end; end;