:: YELLOW_2 semantic presentation begin theorem :: YELLOW_2:1 for L being non empty RelStr for x being Element of L for X being Subset of L holds ( X c= downarrow x iff X is_<=_than x ) proof let L be non empty RelStr ; ::_thesis: for x being Element of L for X being Subset of L holds ( X c= downarrow x iff X is_<=_than x ) let x be Element of L; ::_thesis: for X being Subset of L holds ( X c= downarrow x iff X is_<=_than x ) let X be Subset of L; ::_thesis: ( X c= downarrow x iff X is_<=_than x ) hereby ::_thesis: ( X is_<=_than x implies X c= downarrow x ) assume A1: X c= downarrow x ; ::_thesis: X is_<=_than x thus X is_<=_than x ::_thesis: verum proof let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in X or a <= x ) assume a in X ; ::_thesis: a <= x hence a <= x by A1, WAYBEL_0:17; ::_thesis: verum end; end; assume A2: for a being Element of L st a in X holds a <= x ; :: according to LATTICE3:def_9 ::_thesis: X c= downarrow x let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in downarrow x ) assume A3: a in X ; ::_thesis: a in downarrow x then reconsider a = a as Element of L ; a <= x by A2, A3; hence a in downarrow x by WAYBEL_0:17; ::_thesis: verum end; theorem :: YELLOW_2:2 for L being non empty RelStr for x being Element of L for X being Subset of L holds ( X c= uparrow x iff x is_<=_than X ) proof let L be non empty RelStr ; ::_thesis: for x being Element of L for X being Subset of L holds ( X c= uparrow x iff x is_<=_than X ) let x be Element of L; ::_thesis: for X being Subset of L holds ( X c= uparrow x iff x is_<=_than X ) let X be Subset of L; ::_thesis: ( X c= uparrow x iff x is_<=_than X ) hereby ::_thesis: ( x is_<=_than X implies X c= uparrow x ) assume A1: X c= uparrow x ; ::_thesis: x is_<=_than X thus x is_<=_than X ::_thesis: verum proof let a be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not a in X or x <= a ) assume a in X ; ::_thesis: x <= a hence x <= a by A1, WAYBEL_0:18; ::_thesis: verum end; end; assume A2: for a being Element of L st a in X holds x <= a ; :: according to LATTICE3:def_8 ::_thesis: X c= uparrow x let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in uparrow x ) assume A3: a in X ; ::_thesis: a in uparrow x then reconsider a = a as Element of L ; x <= a by A2, A3; hence a in uparrow x by WAYBEL_0:18; ::_thesis: verum end; theorem :: YELLOW_2:3 for L being transitive antisymmetric with_suprema RelStr for X, Y being set st ex_sup_of X,L & ex_sup_of Y,L holds ( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) ) proof let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for X, Y being set st ex_sup_of X,L & ex_sup_of Y,L holds ( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) ) let X, Y be set ; ::_thesis: ( ex_sup_of X,L & ex_sup_of Y,L implies ( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) ) ) assume that A1: ex_sup_of X,L and A2: ex_sup_of Y,L ; ::_thesis: ( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) ) set a = ("\/" (X,L)) "\/" ("\/" (Y,L)); A3: X \/ Y is_<=_than ("\/" (X,L)) "\/" ("\/" (Y,L)) proof let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X \/ Y or x <= ("\/" (X,L)) "\/" ("\/" (Y,L)) ) assume A4: x in X \/ Y ; ::_thesis: x <= ("\/" (X,L)) "\/" ("\/" (Y,L)) percases ( x in X or x in Y ) by A4, XBOOLE_0:def_3; supposeA5: x in X ; ::_thesis: x <= ("\/" (X,L)) "\/" ("\/" (Y,L)) X is_<=_than "\/" (X,L) by A1, YELLOW_0:30; then A6: x <= "\/" (X,L) by A5, LATTICE3:def_9; "\/" (X,L) <= ("\/" (X,L)) "\/" ("\/" (Y,L)) by YELLOW_0:22; hence x <= ("\/" (X,L)) "\/" ("\/" (Y,L)) by A6, ORDERS_2:3; ::_thesis: verum end; supposeA7: x in Y ; ::_thesis: x <= ("\/" (X,L)) "\/" ("\/" (Y,L)) Y is_<=_than "\/" (Y,L) by A2, YELLOW_0:30; then A8: x <= "\/" (Y,L) by A7, LATTICE3:def_9; "\/" (Y,L) <= ("\/" (X,L)) "\/" ("\/" (Y,L)) by YELLOW_0:22; hence x <= ("\/" (X,L)) "\/" ("\/" (Y,L)) by A8, ORDERS_2:3; ::_thesis: verum end; end; end; for b being Element of L st X \/ Y is_<=_than b holds ("\/" (X,L)) "\/" ("\/" (Y,L)) <= b proof let b be Element of L; ::_thesis: ( X \/ Y is_<=_than b implies ("\/" (X,L)) "\/" ("\/" (Y,L)) <= b ) assume A9: X \/ Y is_<=_than b ; ::_thesis: ("\/" (X,L)) "\/" ("\/" (Y,L)) <= b Y c= X \/ Y by XBOOLE_1:7; then Y is_<=_than b by A9, YELLOW_0:9; then A10: "\/" (Y,L) <= b by A2, YELLOW_0:30; X c= X \/ Y by XBOOLE_1:7; then X is_<=_than b by A9, YELLOW_0:9; then "\/" (X,L) <= b by A1, YELLOW_0:30; hence ("\/" (X,L)) "\/" ("\/" (Y,L)) <= b by A10, YELLOW_0:22; ::_thesis: verum end; hence ( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) ) by A3, YELLOW_0:30; ::_thesis: verum end; theorem :: YELLOW_2:4 for L being transitive antisymmetric with_infima RelStr for X, Y being set st ex_inf_of X,L & ex_inf_of Y,L holds ( ex_inf_of X \/ Y,L & "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) ) proof let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for X, Y being set st ex_inf_of X,L & ex_inf_of Y,L holds ( ex_inf_of X \/ Y,L & "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) ) let X, Y be set ; ::_thesis: ( ex_inf_of X,L & ex_inf_of Y,L implies ( ex_inf_of X \/ Y,L & "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) ) ) assume that A1: ex_inf_of X,L and A2: ex_inf_of Y,L ; ::_thesis: ( ex_inf_of X \/ Y,L & "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) ) set a = ("/\" (X,L)) "/\" ("/\" (Y,L)); A3: X \/ Y is_>=_than ("/\" (X,L)) "/\" ("/\" (Y,L)) proof let x be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not x in X \/ Y or ("/\" (X,L)) "/\" ("/\" (Y,L)) <= x ) assume A4: x in X \/ Y ; ::_thesis: ("/\" (X,L)) "/\" ("/\" (Y,L)) <= x percases ( x in X or x in Y ) by A4, XBOOLE_0:def_3; supposeA5: x in X ; ::_thesis: ("/\" (X,L)) "/\" ("/\" (Y,L)) <= x X is_>=_than "/\" (X,L) by A1, YELLOW_0:31; then A6: x >= "/\" (X,L) by A5, LATTICE3:def_8; "/\" (X,L) >= ("/\" (X,L)) "/\" ("/\" (Y,L)) by YELLOW_0:23; hence ("/\" (X,L)) "/\" ("/\" (Y,L)) <= x by A6, ORDERS_2:3; ::_thesis: verum end; supposeA7: x in Y ; ::_thesis: ("/\" (X,L)) "/\" ("/\" (Y,L)) <= x Y is_>=_than "/\" (Y,L) by A2, YELLOW_0:31; then A8: x >= "/\" (Y,L) by A7, LATTICE3:def_8; "/\" (Y,L) >= ("/\" (X,L)) "/\" ("/\" (Y,L)) by YELLOW_0:23; hence ("/\" (X,L)) "/\" ("/\" (Y,L)) <= x by A8, ORDERS_2:3; ::_thesis: verum end; end; end; for b being Element of L st X \/ Y is_>=_than b holds ("/\" (X,L)) "/\" ("/\" (Y,L)) >= b proof let b be Element of L; ::_thesis: ( X \/ Y is_>=_than b implies ("/\" (X,L)) "/\" ("/\" (Y,L)) >= b ) assume A9: X \/ Y is_>=_than b ; ::_thesis: ("/\" (X,L)) "/\" ("/\" (Y,L)) >= b Y c= X \/ Y by XBOOLE_1:7; then Y is_>=_than b by A9, YELLOW_0:9; then A10: "/\" (Y,L) >= b by A2, YELLOW_0:31; X c= X \/ Y by XBOOLE_1:7; then X is_>=_than b by A9, YELLOW_0:9; then "/\" (X,L) >= b by A1, YELLOW_0:31; hence ("/\" (X,L)) "/\" ("/\" (Y,L)) >= b by A10, YELLOW_0:23; ::_thesis: verum end; hence ( ex_inf_of X \/ Y,L & "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) ) by A3, YELLOW_0:31; ::_thesis: verum end; begin theorem Th5: :: YELLOW_2:5 for R being Relation for X, Y being set st X c= Y holds R |_2 X c= R |_2 Y proof let R be Relation; ::_thesis: for X, Y being set st X c= Y holds R |_2 X c= R |_2 Y let X, Y be set ; ::_thesis: ( X c= Y implies R |_2 X c= R |_2 Y ) assume A1: X c= Y ; ::_thesis: R |_2 X c= R |_2 Y then X |` R c= Y |` R by RELAT_1:100; then A2: (X |` R) | X c= (Y |` R) | X by RELAT_1:76; (Y |` R) | X c= (Y |` R) | Y by A1, RELAT_1:75; then (X |` R) | X c= (Y |` R) | Y by A2, XBOOLE_1:1; then R |_2 X c= (Y |` R) | Y by WELLORD1:10; hence R |_2 X c= R |_2 Y by WELLORD1:10; ::_thesis: verum end; theorem :: YELLOW_2:6 for L being RelStr for S, T being full SubRelStr of L st the carrier of S c= the carrier of T holds the InternalRel of S c= the InternalRel of T proof let L be RelStr ; ::_thesis: for S, T being full SubRelStr of L st the carrier of S c= the carrier of T holds the InternalRel of S c= the InternalRel of T let S1, S2 be full SubRelStr of L; ::_thesis: ( the carrier of S1 c= the carrier of S2 implies the InternalRel of S1 c= the InternalRel of S2 ) ( the InternalRel of S1 = the InternalRel of L |_2 the carrier of S1 & the InternalRel of S2 = the InternalRel of L |_2 the carrier of S2 ) by YELLOW_0:def_14; hence ( the carrier of S1 c= the carrier of S2 implies the InternalRel of S1 c= the InternalRel of S2 ) by Th5; ::_thesis: verum end; theorem Th7: :: YELLOW_2:7 for X being set for L being non empty RelStr for S being non empty SubRelStr of L holds ( ( X is directed Subset of S implies X is directed Subset of L ) & ( X is filtered Subset of S implies X is filtered Subset of L ) ) proof let X be set ; ::_thesis: for L being non empty RelStr for S being non empty SubRelStr of L holds ( ( X is directed Subset of S implies X is directed Subset of L ) & ( X is filtered Subset of S implies X is filtered Subset of L ) ) let L be non empty RelStr ; ::_thesis: for S being non empty SubRelStr of L holds ( ( X is directed Subset of S implies X is directed Subset of L ) & ( X is filtered Subset of S implies X is filtered Subset of L ) ) let S be non empty SubRelStr of L; ::_thesis: ( ( X is directed Subset of S implies X is directed Subset of L ) & ( X is filtered Subset of S implies X is filtered Subset of L ) ) thus ( X is directed Subset of S implies X is directed Subset of L ) ::_thesis: ( X is filtered Subset of S implies X is filtered Subset of L ) proof assume A1: X is directed Subset of S ; ::_thesis: X is directed Subset of L the carrier of S c= the carrier of L by YELLOW_0:def_13; then reconsider X = X as Subset of L by A1, XBOOLE_1: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 ) proof let x, y be Element of L; ::_thesis: ( x in X & y in X implies ex z being Element of L st ( z in X & x <= z & y <= z ) ) assume A2: ( x in X & y in X ) ; ::_thesis: ex z being Element of L st ( z in X & x <= z & y <= z ) then reconsider x9 = x, y9 = y as Element of S by A1; consider z being Element of S such that A3: ( z in X & x9 <= z & y9 <= z ) by A1, A2, WAYBEL_0:def_1; reconsider z = z as Element of L by YELLOW_0:58; take z ; ::_thesis: ( z in X & x <= z & y <= z ) thus ( z in X & x <= z & y <= z ) by A3, YELLOW_0:59; ::_thesis: verum end; hence X is directed Subset of L by WAYBEL_0:def_1; ::_thesis: verum end; thus ( X is filtered Subset of S implies X is filtered Subset of L ) ::_thesis: verum proof assume A4: X is filtered Subset of S ; ::_thesis: X is filtered Subset of L the carrier of S c= the carrier of L by YELLOW_0:def_13; then reconsider X = X as Subset of L by A4, XBOOLE_1: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 & z <= x & z <= y ) proof let x, y be Element of L; ::_thesis: ( x in X & y in X implies ex z being Element of L st ( z in X & z <= x & z <= y ) ) assume A5: ( x in X & y in X ) ; ::_thesis: ex z being Element of L st ( z in X & z <= x & z <= y ) then reconsider x9 = x, y9 = y as Element of S by A4; consider z being Element of S such that A6: ( z in X & z <= x9 & z <= y9 ) by A4, A5, WAYBEL_0:def_2; reconsider z = z as Element of L by YELLOW_0:58; take z ; ::_thesis: ( z in X & z <= x & z <= y ) thus ( z in X & z <= x & z <= y ) by A6, YELLOW_0:59; ::_thesis: verum end; hence X is filtered Subset of L by WAYBEL_0:def_2; ::_thesis: verum end; end; theorem :: YELLOW_2:8 for L being non empty RelStr for S, T being non empty full SubRelStr of L st the carrier of S c= the carrier of T holds for X being Subset of S holds ( X is Subset of T & ( for Y being Subset of T st X = Y holds ( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) ) proof let L be non empty RelStr ; ::_thesis: for S, T being non empty full SubRelStr of L st the carrier of S c= the carrier of T holds for X being Subset of S holds ( X is Subset of T & ( for Y being Subset of T st X = Y holds ( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) ) let S1, S2 be non empty full SubRelStr of L; ::_thesis: ( the carrier of S1 c= the carrier of S2 implies for X being Subset of S1 holds ( X is Subset of S2 & ( for Y being Subset of S2 st X = Y holds ( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) ) ) assume A1: the carrier of S1 c= the carrier of S2 ; ::_thesis: for X being Subset of S1 holds ( X is Subset of S2 & ( for Y being Subset of S2 st X = Y holds ( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) ) let X be Subset of S1; ::_thesis: ( X is Subset of S2 & ( for Y being Subset of S2 st X = Y holds ( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) ) thus X is Subset of S2 by A1, XBOOLE_1:1; ::_thesis: for Y being Subset of S2 st X = Y holds ( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) let X2 be Subset of S2; ::_thesis: ( X = X2 implies ( ( X is filtered implies X2 is filtered ) & ( X is directed implies X2 is directed ) ) ) assume A2: X = X2 ; ::_thesis: ( ( X is filtered implies X2 is filtered ) & ( X is directed implies X2 is directed ) ) hereby ::_thesis: ( X is directed implies X2 is directed ) assume A3: X is filtered ; ::_thesis: X2 is filtered thus X2 is filtered ::_thesis: verum proof let x, y be Element of S2; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in X2 or not y in X2 or ex b1 being Element of the carrier of S2 st ( b1 in X2 & b1 <= x & b1 <= y ) ) assume A4: ( x in X2 & y in X2 ) ; ::_thesis: ex b1 being Element of the carrier of S2 st ( b1 in X2 & b1 <= x & b1 <= y ) then reconsider x9 = x, y9 = y as Element of S1 by A2; consider z being Element of S1 such that A5: z in X and A6: ( z <= x9 & z <= y9 ) by A2, A3, A4, WAYBEL_0:def_2; reconsider x1 = x, y1 = y, z1 = z as Element of L by YELLOW_0:58; reconsider z = z as Element of S2 by A2, A5; take z ; ::_thesis: ( z in X2 & z <= x & z <= y ) ( z1 <= x1 & z1 <= y1 ) by A6, YELLOW_0:59; hence ( z in X2 & z <= x & z <= y ) by A2, A5, YELLOW_0:60; ::_thesis: verum end; end; assume A7: X is directed ; ::_thesis: X2 is directed let x, y be Element of S2; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in X2 or not y in X2 or ex b1 being Element of the carrier of S2 st ( b1 in X2 & x <= b1 & y <= b1 ) ) assume A8: ( x in X2 & y in X2 ) ; ::_thesis: ex b1 being Element of the carrier of S2 st ( b1 in X2 & x <= b1 & y <= b1 ) then reconsider x9 = x, y9 = y as Element of S1 by A2; consider z being Element of S1 such that A9: z in X and A10: ( x9 <= z & y9 <= z ) by A2, A7, A8, WAYBEL_0:def_1; reconsider x1 = x, y1 = y, z1 = z as Element of L by YELLOW_0:58; reconsider z = z as Element of S2 by A2, A9; take z ; ::_thesis: ( z in X2 & x <= z & y <= z ) ( x1 <= z1 & y1 <= z1 ) by A10, YELLOW_0:59; hence ( z in X2 & x <= z & y <= z ) by A2, A9, YELLOW_0:60; ::_thesis: verum end; begin definition let J be set ; let L be RelStr ; let f, g be Function of J, the carrier of L; predf <= g means :Def1: :: YELLOW_2:def 1 for j being set st j in J holds ex a, b being Element of L st ( a = f . j & b = g . j & a <= b ); end; :: deftheorem Def1 defines <= YELLOW_2:def_1_:_ for J being set for L being RelStr for f, g being Function of J, the carrier of L holds ( f <= g iff for j being set st j in J holds ex a, b being Element of L st ( a = f . j & b = g . j & a <= b ) ); notation let J be set ; let L be RelStr ; let f, g be Function of J, the carrier of L; synonym g >= f for f <= g; end; theorem :: YELLOW_2:9 for L, M being non empty RelStr for f, g being Function of L,M holds ( f <= g iff for x being Element of L holds f . x <= g . x ) proof let L, M be non empty RelStr ; ::_thesis: for f, g being Function of L,M holds ( f <= g iff for x being Element of L holds f . x <= g . x ) let f, g be Function of L,M; ::_thesis: ( f <= g iff for x being Element of L holds f . x <= g . x ) hereby ::_thesis: ( ( for x being Element of L holds f . x <= g . x ) implies f <= g ) assume A1: f <= g ; ::_thesis: for x being Element of L holds f . x <= g . x let x be Element of L; ::_thesis: f . x <= g . x ex m1, m2 being Element of M st ( m1 = f . x & m2 = g . x & m1 <= m2 ) by A1, Def1; hence f . x <= g . x ; ::_thesis: verum end; assume A2: for x being Element of L holds f . x <= g . x ; ::_thesis: f <= g let x be set ; :: according to YELLOW_2:def_1 ::_thesis: ( x in the carrier of L implies ex a, b being Element of M st ( a = f . x & b = g . x & a <= b ) ) assume x in the carrier of L ; ::_thesis: ex a, b being Element of M st ( a = f . x & b = g . x & a <= b ) then reconsider x = x as Element of L ; take f . x ; ::_thesis: ex b being Element of M st ( f . x = f . x & b = g . x & f . x <= b ) take g . x ; ::_thesis: ( f . x = f . x & g . x = g . x & f . x <= g . x ) thus ( f . x = f . x & g . x = g . x & f . x <= g . x ) by A2; ::_thesis: verum end; begin definition let L, M be non empty RelStr ; let f be Function of L,M; func Image f -> strict full SubRelStr of M equals :: YELLOW_2:def 2 subrelstr (rng f); correctness coherence subrelstr (rng f) is strict full SubRelStr of M; ; end; :: deftheorem defines Image YELLOW_2:def_2_:_ for L, M being non empty RelStr for f being Function of L,M holds Image f = subrelstr (rng f); theorem :: YELLOW_2:10 for L, M being non empty RelStr for f being Function of L,M for y being Element of (Image f) ex x being Element of L st f . x = y proof let L1, L2 be non empty RelStr ; ::_thesis: for f being Function of L1,L2 for y being Element of (Image f) ex x being Element of L1 st f . x = y let g be Function of L1,L2; ::_thesis: for y being Element of (Image g) ex x being Element of L1 st g . x = y let s be Element of (Image g); ::_thesis: ex x being Element of L1 st g . x = s dom g = the carrier of L1 by FUNCT_2:def_1; then A1: not rng g is empty by RELAT_1:42; rng g = the carrier of (Image g) by YELLOW_0:def_15; then consider l being set such that A2: l in dom g and A3: s = g . l by A1, FUNCT_1:def_3; reconsider l = l as Element of L1 by A2; take l ; ::_thesis: g . l = s thus g . l = s by A3; ::_thesis: verum end; registration let L be non empty RelStr ; let X be non empty Subset of L; cluster subrelstr X -> non empty ; coherence not subrelstr X is empty by YELLOW_0:def_15; end; registration let L, M be non empty RelStr ; let f be Function of L,M; cluster Image f -> non empty strict full ; coherence not Image f is empty proof dom f = the carrier of L by FUNCT_2:def_1; then not rng f is empty by RELAT_1:42; hence not Image f is empty ; ::_thesis: verum end; end; begin theorem :: YELLOW_2:11 for L being non empty RelStr holds id L is monotone proof let L be non empty RelStr ; ::_thesis: id L is monotone let l1, l2 be Element of L; :: according to ORDERS_3:def_5 ::_thesis: ( not l1 <= l2 or for b1, b2 being Element of the carrier of L holds ( not b1 = (id L) . l1 or not b2 = (id L) . l2 or b1 <= b2 ) ) assume l1 <= l2 ; ::_thesis: for b1, b2 being Element of the carrier of L holds ( not b1 = (id L) . l1 or not b2 = (id L) . l2 or b1 <= b2 ) then l1 <= (id L) . l2 by FUNCT_1:18; hence for b1, b2 being Element of the carrier of L holds ( not b1 = (id L) . l1 or not b2 = (id L) . l2 or b1 <= b2 ) by FUNCT_1:18; ::_thesis: verum end; theorem :: YELLOW_2:12 for L, M, N being non empty RelStr for f being Function of L,M for g being Function of M,N st f is monotone & g is monotone holds g * f is monotone proof let L1, L2, L3 be non empty RelStr ; ::_thesis: for f being Function of L1,L2 for g being Function of L2,L3 st f is monotone & g is monotone holds g * f is monotone let g1 be Function of L1,L2; ::_thesis: for g being Function of L2,L3 st g1 is monotone & g is monotone holds g * g1 is monotone let g2 be Function of L2,L3; ::_thesis: ( g1 is monotone & g2 is monotone implies g2 * g1 is monotone ) assume that A1: g1 is monotone and A2: g2 is monotone ; ::_thesis: g2 * g1 is monotone let s1, s2 be Element of L1; :: according to ORDERS_3:def_5 ::_thesis: ( not s1 <= s2 or for b1, b2 being Element of the carrier of L3 holds ( not b1 = (g2 * g1) . s1 or not b2 = (g2 * g1) . s2 or b1 <= b2 ) ) assume s1 <= s2 ; ::_thesis: for b1, b2 being Element of the carrier of L3 holds ( not b1 = (g2 * g1) . s1 or not b2 = (g2 * g1) . s2 or b1 <= b2 ) then g1 . s1 <= g1 . s2 by A1, ORDERS_3:def_5; then g2 . (g1 . s1) <= g2 . (g1 . s2) by A2, ORDERS_3:def_5; then (g2 * g1) . s1 <= g2 . (g1 . s2) by FUNCT_2:15; hence for b1, b2 being Element of the carrier of L3 holds ( not b1 = (g2 * g1) . s1 or not b2 = (g2 * g1) . s2 or b1 <= b2 ) by FUNCT_2:15; ::_thesis: verum end; theorem :: YELLOW_2:13 for L, M being non empty RelStr for f being Function of L,M for X being Subset of L for x being Element of L st f is monotone & x is_<=_than X holds f . x is_<=_than f .: X proof let L1, L2 be non empty RelStr ; ::_thesis: for f being Function of L1,L2 for X being Subset of L1 for x being Element of L1 st f is monotone & x is_<=_than X holds f . x is_<=_than f .: X let g be Function of L1,L2; ::_thesis: for X being Subset of L1 for x being Element of L1 st g is monotone & x is_<=_than X holds g . x is_<=_than g .: X let X be Subset of L1; ::_thesis: for x being Element of L1 st g is monotone & x is_<=_than X holds g . x is_<=_than g .: X let x be Element of L1; ::_thesis: ( g is monotone & x is_<=_than X implies g . x is_<=_than g .: X ) assume that A1: g is monotone and A2: x is_<=_than X ; ::_thesis: g . x is_<=_than g .: X let y2 be Element of L2; :: according to LATTICE3:def_8 ::_thesis: ( not y2 in g .: X or g . x <= y2 ) assume y2 in g .: X ; ::_thesis: g . x <= y2 then consider x2 being Element of L1 such that A3: x2 in X and A4: y2 = g . x2 by FUNCT_2:65; reconsider x2 = x2 as Element of L1 ; x <= x2 by A2, A3, LATTICE3:def_8; hence g . x <= y2 by A1, A4, ORDERS_3:def_5; ::_thesis: verum end; theorem :: YELLOW_2:14 for L, M being non empty RelStr for f being Function of L,M for X being Subset of L for x being Element of L st f is monotone & X is_<=_than x holds f .: X is_<=_than f . x proof let L1, L2 be non empty RelStr ; ::_thesis: for f being Function of L1,L2 for X being Subset of L1 for x being Element of L1 st f is monotone & X is_<=_than x holds f .: X is_<=_than f . x let g be Function of L1,L2; ::_thesis: for X being Subset of L1 for x being Element of L1 st g is monotone & X is_<=_than x holds g .: X is_<=_than g . x let X be Subset of L1; ::_thesis: for x being Element of L1 st g is monotone & X is_<=_than x holds g .: X is_<=_than g . x let x be Element of L1; ::_thesis: ( g is monotone & X is_<=_than x implies g .: X is_<=_than g . x ) assume that A1: g is monotone and A2: x is_>=_than X ; ::_thesis: g .: X is_<=_than g . x let y2 be Element of L2; :: according to LATTICE3:def_9 ::_thesis: ( not y2 in g .: X or y2 <= g . x ) assume y2 in g .: X ; ::_thesis: y2 <= g . x then consider x2 being Element of L1 such that A3: x2 in X and A4: y2 = g . x2 by FUNCT_2:65; reconsider x2 = x2 as Element of L1 ; x >= x2 by A2, A3, LATTICE3:def_9; hence y2 <= g . x by A1, A4, ORDERS_3:def_5; ::_thesis: verum end; theorem :: YELLOW_2:15 for S, T being non empty RelStr for f being Function of S,T for X being directed Subset of S st f is monotone holds f .: X is directed proof let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T for X being directed Subset of S st f is monotone holds f .: X is directed let f be Function of S,T; ::_thesis: for X being directed Subset of S st f is monotone holds f .: X is directed let X be directed Subset of S; ::_thesis: ( f is monotone implies f .: X is directed ) set Y = f .: X; assume A1: f is monotone ; ::_thesis: f .: X is directed for y1, y2 being Element of T st y1 in f .: X & y2 in f .: X holds ex z being Element of T st ( z in f .: X & y1 <= z & y2 <= z ) proof let y1, y2 be Element of T; ::_thesis: ( y1 in f .: X & y2 in f .: X implies ex z being Element of T st ( z in f .: X & y1 <= z & y2 <= z ) ) assume that A2: y1 in f .: X and A3: y2 in f .: X ; ::_thesis: ex z being Element of T st ( z in f .: X & y1 <= z & y2 <= z ) consider x1 being set such that x1 in dom f and A4: x1 in X and A5: y1 = f . x1 by A2, FUNCT_1:def_6; consider x2 being set such that x2 in dom f and A6: x2 in X and A7: y2 = f . x2 by A3, FUNCT_1:def_6; reconsider x1 = x1, x2 = x2 as Element of S by A4, A6; consider z being Element of S such that A8: z in X and A9: ( x1 <= z & x2 <= z ) by A4, A6, WAYBEL_0:def_1; take f . z ; ::_thesis: ( f . z in f .: X & y1 <= f . z & y2 <= f . z ) thus f . z in f .: X by A8, FUNCT_2:35; ::_thesis: ( y1 <= f . z & y2 <= f . z ) thus ( y1 <= f . z & y2 <= f . z ) by A1, A5, A7, A9, ORDERS_3:def_5; ::_thesis: verum end; hence f .: X is directed by WAYBEL_0:def_1; ::_thesis: verum end; theorem Th16: :: YELLOW_2:16 for L being with_suprema Poset for f being Function of L,L st f is directed-sups-preserving holds f is monotone proof let L be with_suprema Poset; ::_thesis: for f being Function of L,L st f is directed-sups-preserving holds f is monotone let f be Function of L,L; ::_thesis: ( f is directed-sups-preserving implies f is monotone ) assume A1: f is directed-sups-preserving ; ::_thesis: f is monotone let x, y be Element of L; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) ) assume A2: x <= y ; ::_thesis: for b1, b2 being Element of the carrier of L holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) A3: y = y "\/" x by A2, YELLOW_0:24; for a, b being Element of L st a in {x,y} & b in {x,y} holds ex z being Element of L st ( z in {x,y} & a <= z & b <= z ) proof let a, b be Element of L; ::_thesis: ( a in {x,y} & b in {x,y} implies ex z being Element of L st ( z in {x,y} & a <= z & b <= z ) ) assume A4: ( a in {x,y} & b in {x,y} ) ; ::_thesis: ex z being Element of L st ( z in {x,y} & a <= z & b <= z ) take y ; ::_thesis: ( y in {x,y} & a <= y & b <= y ) thus y in {x,y} by TARSKI:def_2; ::_thesis: ( a <= y & b <= y ) thus ( a <= y & b <= y ) by A2, A4, TARSKI:def_2; ::_thesis: verum end; then ( {x,y} is directed & not {x,y} is empty ) by WAYBEL_0:def_1; then A5: f preserves_sup_of {x,y} by A1, WAYBEL_0:def_37; A6: dom f = the carrier of L by FUNCT_2:def_1; y <= y ; then A7: {x,y} is_<=_than y by A2, YELLOW_0:8; for b being Element of L st {x,y} is_<=_than b holds y <= b by YELLOW_0:8; then ex_sup_of {x,y},L by A7, YELLOW_0:30; then sup (f .: {x,y}) = f . (sup {x,y}) by A5, WAYBEL_0:def_31 .= f . y by A3, YELLOW_0:41 ; then A8: f . y = sup {(f . x),(f . y)} by A6, FUNCT_1:60 .= (f . y) "\/" (f . x) by YELLOW_0:41 ; let afx, bfy be Element of L; ::_thesis: ( not afx = f . x or not bfy = f . y or afx <= bfy ) assume ( afx = f . x & bfy = f . y ) ; ::_thesis: afx <= bfy hence afx <= bfy by A8, YELLOW_0:22; ::_thesis: verum end; theorem :: YELLOW_2:17 for L being with_infima Poset for f being Function of L,L st f is filtered-infs-preserving holds f is monotone proof let L be with_infima Poset; ::_thesis: for f being Function of L,L st f is filtered-infs-preserving holds f is monotone let f be Function of L,L; ::_thesis: ( f is filtered-infs-preserving implies f is monotone ) assume A1: f is filtered-infs-preserving ; ::_thesis: f is monotone let x, y be Element of L; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) ) assume A2: x <= y ; ::_thesis: for b1, b2 being Element of the carrier of L holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) A3: x = x "/\" y by A2, YELLOW_0:25; for c, d being Element of L st c in {x,y} & d in {x,y} holds ex z being Element of L st ( z in {x,y} & z <= c & z <= d ) proof let c, d be Element of L; ::_thesis: ( c in {x,y} & d in {x,y} implies ex z being Element of L st ( z in {x,y} & z <= c & z <= d ) ) assume A4: ( c in {x,y} & d in {x,y} ) ; ::_thesis: ex z being Element of L st ( z in {x,y} & z <= c & z <= d ) take x ; ::_thesis: ( x in {x,y} & x <= c & x <= d ) thus x in {x,y} by TARSKI:def_2; ::_thesis: ( x <= c & x <= d ) thus ( x <= c & x <= d ) by A2, A4, TARSKI:def_2; ::_thesis: verum end; then ( {x,y} is filtered & not {x,y} is empty ) by WAYBEL_0:def_2; then A5: f preserves_inf_of {x,y} by A1, WAYBEL_0:def_36; A6: dom f = the carrier of L by FUNCT_2:def_1; x <= x ; then A7: x is_<=_than {x,y} by A2, YELLOW_0:8; for c being Element of L st c is_<=_than {x,y} holds c <= x by YELLOW_0:8; then ex_inf_of {x,y},L by A7, YELLOW_0:31; then inf (f .: {x,y}) = f . (inf {x,y}) by A5, WAYBEL_0:def_30 .= f . x by A3, YELLOW_0:40 ; then A8: f . x = inf {(f . x),(f . y)} by A6, FUNCT_1:60 .= (f . x) "/\" (f . y) by YELLOW_0:40 ; let a, b be Element of L; ::_thesis: ( not a = f . x or not b = f . y or a <= b ) assume ( a = f . x & b = f . y ) ; ::_thesis: a <= b hence a <= b by A8, YELLOW_0:23; ::_thesis: verum end; begin theorem :: YELLOW_2:18 for S being non empty 1-sorted for f being Function of S,S st f is idempotent holds for x being Element of S holds f . (f . x) = f . x proof let L be non empty 1-sorted ; ::_thesis: for f being Function of L,L st f is idempotent holds for x being Element of L holds f . (f . x) = f . x let p be Function of L,L; ::_thesis: ( p is idempotent implies for x being Element of L holds p . (p . x) = p . x ) assume A1: p * p = p ; :: according to QUANTAL1:def_9 ::_thesis: for x being Element of L holds p . (p . x) = p . x let l be Element of L; ::_thesis: p . (p . l) = p . l thus p . (p . l) = p . l by A1, FUNCT_2:15; ::_thesis: verum end; theorem Th19: :: YELLOW_2:19 for S being non empty 1-sorted for f being Function of S,S st f is idempotent holds rng f = { x where x is Element of S : x = f . x } proof let S be non empty 1-sorted ; ::_thesis: for f being Function of S,S st f is idempotent holds rng f = { x where x is Element of S : x = f . x } let f be Function of S,S; ::_thesis: ( f is idempotent implies rng f = { x where x is Element of S : x = f . x } ) set M = { x where x is Element of S : x = f . x } ; assume A1: f = f * f ; :: according to QUANTAL1:def_9 ::_thesis: rng f = { x where x is Element of S : x = f . x } A2: rng f c= { x where x is Element of S : x = f . x } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in { x where x is Element of S : x = f . x } ) assume A3: y in rng f ; ::_thesis: y in { x where x is Element of S : x = f . x } then reconsider y9 = y as Element of S ; ex x being set st ( x in dom f & y = f . x ) by A3, FUNCT_1:def_3; then y9 = f . y9 by A1, FUNCT_1:13; hence y in { x where x is Element of S : x = f . x } ; ::_thesis: verum end; { x where x is Element of S : x = f . x } c= rng f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { x where x is Element of S : x = f . x } or y in rng f ) assume y in { x where x is Element of S : x = f . x } ; ::_thesis: y in rng f then A4: ex y9 being Element of S st ( y9 = y & y9 = f . y9 ) ; dom f = the carrier of S by FUNCT_2:def_1; hence y in rng f by A4, FUNCT_1:def_3; ::_thesis: verum end; hence rng f = { x where x is Element of S : x = f . x } by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th20: :: YELLOW_2:20 for X being set for S being non empty 1-sorted for f being Function of S,S st f is idempotent & X c= rng f holds f .: X = X proof let X be set ; ::_thesis: for S being non empty 1-sorted for f being Function of S,S st f is idempotent & X c= rng f holds f .: X = X let S be non empty 1-sorted ; ::_thesis: for f being Function of S,S st f is idempotent & X c= rng f holds f .: X = X let f be Function of S,S; ::_thesis: ( f is idempotent & X c= rng f implies f .: X = X ) assume A1: f is idempotent ; ::_thesis: ( not X c= rng f or f .: X = X ) set M = { x where x is Element of S : x = f . x } ; assume X c= rng f ; ::_thesis: f .: X = X then A2: X c= { x where x is Element of S : x = f . x } by A1, Th19; A3: f .: X c= X proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: X or y in X ) assume y in f .: X ; ::_thesis: y in X then consider x being set such that x in dom f and A4: x in X and A5: y = f . x by FUNCT_1:def_6; x in { x where x is Element of S : x = f . x } by A2, A4; then ex x9 being Element of S st ( x9 = x & x9 = f . x9 ) ; hence y in X by A4, A5; ::_thesis: verum end; X c= f .: X proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in f .: X ) assume A6: y in X ; ::_thesis: y in f .: X then y in { x where x is Element of S : x = f . x } by A2; then ex x being Element of S st ( x = y & x = f . x ) ; hence y in f .: X by A6, FUNCT_2:35; ::_thesis: verum end; hence f .: X = X by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: YELLOW_2:21 for L being non empty RelStr holds id L is idempotent proof let L be non empty RelStr ; ::_thesis: id L is idempotent thus (id L) * (id L) = id ( the carrier of L /\ the carrier of L) by FUNCT_1:22 .= id L ; :: according to QUANTAL1:def_9 ::_thesis: verum end; begin theorem Th22: :: YELLOW_2:22 for X being set for L being complete LATTICE for a being Element of L st a in X holds ( a <= "\/" (X,L) & "/\" (X,L) <= a ) proof let X be set ; ::_thesis: for L being complete LATTICE for a being Element of L st a in X holds ( a <= "\/" (X,L) & "/\" (X,L) <= a ) let L be complete LATTICE; ::_thesis: for a being Element of L st a in X holds ( a <= "\/" (X,L) & "/\" (X,L) <= a ) let a be Element of L; ::_thesis: ( a in X implies ( a <= "\/" (X,L) & "/\" (X,L) <= a ) ) assume A1: a in X ; ::_thesis: ( a <= "\/" (X,L) & "/\" (X,L) <= a ) X is_<=_than "\/" (X,L) by YELLOW_0:32; hence a <= "\/" (X,L) by A1, LATTICE3:def_9; ::_thesis: "/\" (X,L) <= a X is_>=_than "/\" (X,L) by YELLOW_0:33; hence "/\" (X,L) <= a by A1, LATTICE3:def_8; ::_thesis: verum end; theorem Th23: :: YELLOW_2:23 for L being non empty RelStr holds ( ( for X being set holds ex_sup_of X,L ) iff for Y being set holds ex_inf_of Y,L ) proof let L be non empty RelStr ; ::_thesis: ( ( for X being set holds ex_sup_of X,L ) iff for Y being set holds ex_inf_of Y,L ) hereby ::_thesis: ( ( for Y being set holds ex_inf_of Y,L ) implies for X being set holds ex_sup_of X,L ) assume A1: for X being set holds ex_sup_of X,L ; ::_thesis: for Y being set holds ex_inf_of Y,L let Y be set ; ::_thesis: ex_inf_of Y,L set X = { x where x is Element of L : x is_<=_than Y } ; ex_sup_of { x where x is Element of L : x is_<=_than Y } ,L by A1; then consider a being Element of L such that A2: { x where x is Element of L : x is_<=_than Y } is_<=_than a and A3: for b being Element of L st { x where x is Element of L : x is_<=_than Y } is_<=_than b holds b >= a and A4: for c being Element of L st { x where x is Element of L : x is_<=_than Y } is_<=_than c & ( for b being Element of L st { x where x is Element of L : x is_<=_than Y } is_<=_than b holds b >= c ) holds c = a by YELLOW_0:def_7; A5: a is_<=_than Y proof let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in Y or a <= b ) assume A6: b in Y ; ::_thesis: a <= b b is_>=_than { x where x is Element of L : x is_<=_than Y } proof let c be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not c in { x where x is Element of L : x is_<=_than Y } or c <= b ) assume c in { x where x is Element of L : x is_<=_than Y } ; ::_thesis: c <= b then ex x being Element of L st ( c = x & x is_<=_than Y ) ; hence c <= b by A6, LATTICE3:def_8; ::_thesis: verum end; hence a <= b by A3; ::_thesis: verum end; A7: for c being Element of L st Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds b <= c ) holds c = a proof let c be Element of L; ::_thesis: ( Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds b <= c ) implies c = a ) assume that A8: Y is_>=_than c and A9: for b being Element of L st Y is_>=_than b holds b <= c ; ::_thesis: c = a A10: for b being Element of L st { x where x is Element of L : x is_<=_than Y } is_<=_than b holds b >= c proof let b be Element of L; ::_thesis: ( { x where x is Element of L : x is_<=_than Y } is_<=_than b implies b >= c ) assume A11: { x where x is Element of L : x is_<=_than Y } is_<=_than b ; ::_thesis: b >= c c in { x where x is Element of L : x is_<=_than Y } by A8; hence b >= c by A11, LATTICE3:def_9; ::_thesis: verum end; { x where x is Element of L : x is_<=_than Y } is_<=_than c proof let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in { x where x is Element of L : x is_<=_than Y } or b <= c ) assume b in { x where x is Element of L : x is_<=_than Y } ; ::_thesis: b <= c then ex x being Element of L st ( b = x & x is_<=_than Y ) ; hence b <= c by A9; ::_thesis: verum end; hence c = a by A4, A10; ::_thesis: verum end; for b being Element of L st Y is_>=_than b holds a >= b proof let b be Element of L; ::_thesis: ( Y is_>=_than b implies a >= b ) assume b is_<=_than Y ; ::_thesis: a >= b then b in { x where x is Element of L : x is_<=_than Y } ; hence a >= b by A2, LATTICE3:def_9; ::_thesis: verum end; hence ex_inf_of Y,L by A5, A7, YELLOW_0:def_8; ::_thesis: verum end; assume A12: for Y being set holds ex_inf_of Y,L ; ::_thesis: for X being set holds ex_sup_of X,L let X be set ; ::_thesis: ex_sup_of X,L set Y = { y where y is Element of L : X is_<=_than y } ; ex_inf_of { y where y is Element of L : X is_<=_than y } ,L by A12; then consider a being Element of L such that A13: { y where y is Element of L : X is_<=_than y } is_>=_than a and A14: for b being Element of L st { y where y is Element of L : X is_<=_than y } is_>=_than b holds b <= a and A15: for c being Element of L st { y where y is Element of L : X is_<=_than y } is_>=_than c & ( for b being Element of L st { y where y is Element of L : X is_<=_than y } is_>=_than b holds b <= c ) holds c = a by YELLOW_0:def_8; A16: X is_<=_than a proof let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in X or b <= a ) assume A17: b in X ; ::_thesis: b <= a b is_<=_than { y where y is Element of L : X is_<=_than y } proof let c be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not c in { y where y is Element of L : X is_<=_than y } or b <= c ) assume c in { y where y is Element of L : X is_<=_than y } ; ::_thesis: b <= c then ex y being Element of L st ( c = y & X is_<=_than y ) ; hence b <= c by A17, LATTICE3:def_9; ::_thesis: verum end; hence b <= a by A14; ::_thesis: verum end; A18: 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 proof let c be Element of L; ::_thesis: ( X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) implies c = a ) assume that A19: X is_<=_than c and A20: for b being Element of L st X is_<=_than b holds b >= c ; ::_thesis: c = a A21: for b being Element of L st { y where y is Element of L : X is_<=_than y } is_>=_than b holds b <= c proof let b be Element of L; ::_thesis: ( { y where y is Element of L : X is_<=_than y } is_>=_than b implies b <= c ) assume A22: { y where y is Element of L : X is_<=_than y } is_>=_than b ; ::_thesis: b <= c c in { y where y is Element of L : X is_<=_than y } by A19; hence b <= c by A22, LATTICE3:def_8; ::_thesis: verum end; { y where y is Element of L : X is_<=_than y } is_>=_than c proof let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in { y where y is Element of L : X is_<=_than y } or c <= b ) assume b in { y where y is Element of L : X is_<=_than y } ; ::_thesis: c <= b then ex x being Element of L st ( b = x & x is_>=_than X ) ; hence c <= b by A20; ::_thesis: verum end; hence c = a by A15, A21; ::_thesis: verum end; for b being Element of L st X is_<=_than b holds a <= b proof let b be Element of L; ::_thesis: ( X is_<=_than b implies a <= b ) assume X is_<=_than b ; ::_thesis: a <= b then b in { y where y is Element of L : X is_<=_than y } ; hence a <= b by A13, LATTICE3:def_8; ::_thesis: verum end; hence ex_sup_of X,L by A16, A18, YELLOW_0:def_7; ::_thesis: verum end; theorem Th24: :: YELLOW_2:24 for L being non empty RelStr st ( for X being set holds ex_sup_of X,L ) holds L is complete proof let L be non empty RelStr ; ::_thesis: ( ( for X being set holds ex_sup_of X,L ) implies L is complete ) assume A1: for X being set holds ex_sup_of X,L ; ::_thesis: L is complete L is complete proof 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 ) ) ) take a = "\/" (X,L); ::_thesis: ( X is_<=_than a & ( for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or a <= b1 ) ) ) A2: ex_sup_of X,L by A1; hence X is_<=_than a by YELLOW_0:def_9; ::_thesis: for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or a <= b1 ) thus for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or a <= b1 ) by A2, YELLOW_0:def_9; ::_thesis: verum end; hence L is complete ; ::_thesis: verum end; theorem Th25: :: YELLOW_2:25 for L being non empty RelStr st ( for X being set holds ex_inf_of X,L ) holds L is complete proof let L be non empty RelStr ; ::_thesis: ( ( for X being set holds ex_inf_of X,L ) implies L is complete ) assume for X being set holds ex_inf_of X,L ; ::_thesis: L is complete then for X being set holds ex_sup_of X,L by Th23; hence L is complete by Th24; ::_thesis: verum end; theorem Th26: :: YELLOW_2:26 for L being non empty RelStr st ( for A being Subset of L holds ex_inf_of A,L ) holds for X being set holds ( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) ) proof let L be non empty RelStr ; ::_thesis: ( ( for A being Subset of L holds ex_inf_of A,L ) implies for X being set holds ( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) ) ) assume A1: for A being Subset of L holds ex_inf_of A,L ; ::_thesis: for X being set holds ( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) ) let X be set ; ::_thesis: ( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) ) set Y = X /\ the carrier of L; set a = "/\" ((X /\ the carrier of L),L); reconsider Y = X /\ the carrier of L as Subset of L by XBOOLE_1:17; A2: ex_inf_of Y,L by A1; A3: "/\" ((X /\ the carrier of L),L) is_<=_than X proof let x be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not x in X or "/\" ((X /\ the carrier of L),L) <= x ) assume x in X ; ::_thesis: "/\" ((X /\ the carrier of L),L) <= x then A4: x in Y by XBOOLE_0:def_4; "/\" ((X /\ the carrier of L),L) is_<=_than Y by A2, YELLOW_0:def_10; hence "/\" ((X /\ the carrier of L),L) <= x by A4, LATTICE3:def_8; ::_thesis: verum end; A5: for b being Element of L st b is_<=_than X holds b <= "/\" ((X /\ the carrier of L),L) proof let b be Element of L; ::_thesis: ( b is_<=_than X implies b <= "/\" ((X /\ the carrier of L),L) ) A6: Y c= X by XBOOLE_1:17; assume b is_<=_than X ; ::_thesis: b <= "/\" ((X /\ the carrier of L),L) then b is_<=_than Y by A6, YELLOW_0:9; hence b <= "/\" ((X /\ the carrier of L),L) by A2, YELLOW_0:def_10; ::_thesis: verum end; ex_inf_of X,L by A2, YELLOW_0:50; hence ( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) ) by A3, A5, YELLOW_0:def_10; ::_thesis: verum end; theorem :: YELLOW_2:27 for L being non empty RelStr st ( for A being Subset of L holds ex_sup_of A,L ) holds for X being set holds ( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) ) proof let L be non empty RelStr ; ::_thesis: ( ( for A being Subset of L holds ex_sup_of A,L ) implies for X being set holds ( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) ) ) assume A1: for A being Subset of L holds ex_sup_of A,L ; ::_thesis: for X being set holds ( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) ) let X be set ; ::_thesis: ( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) ) set Y = X /\ the carrier of L; set a = "\/" ((X /\ the carrier of L),L); reconsider Y = X /\ the carrier of L as Subset of L by XBOOLE_1:17; A2: ex_sup_of Y,L by A1; A3: X is_<=_than "\/" ((X /\ the carrier of L),L) proof let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= "\/" ((X /\ the carrier of L),L) ) assume x in X ; ::_thesis: x <= "\/" ((X /\ the carrier of L),L) then A4: x in Y by XBOOLE_0:def_4; Y is_<=_than "\/" ((X /\ the carrier of L),L) by A2, YELLOW_0:def_9; hence x <= "\/" ((X /\ the carrier of L),L) by A4, LATTICE3:def_9; ::_thesis: verum end; A5: for b being Element of L st X is_<=_than b holds "\/" ((X /\ the carrier of L),L) <= b proof let b be Element of L; ::_thesis: ( X is_<=_than b implies "\/" ((X /\ the carrier of L),L) <= b ) A6: Y c= X by XBOOLE_1:17; assume X is_<=_than b ; ::_thesis: "\/" ((X /\ the carrier of L),L) <= b then Y is_<=_than b by A6, YELLOW_0:9; hence "\/" ((X /\ the carrier of L),L) <= b by A2, YELLOW_0:def_9; ::_thesis: verum end; ex_sup_of X,L by A2, YELLOW_0:50; hence ( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) ) by A3, A5, YELLOW_0:def_9; ::_thesis: verum end; theorem Th28: :: YELLOW_2:28 for L being non empty RelStr st ( for A being Subset of L holds ex_inf_of A,L ) holds L is complete proof let L be non empty RelStr ; ::_thesis: ( ( for A being Subset of L holds ex_inf_of A,L ) implies L is complete ) assume for A being Subset of L holds ex_inf_of A,L ; ::_thesis: L is complete then for X being set holds ex_inf_of X,L by Th26; hence L is complete by Th25; ::_thesis: verum end; registration cluster non empty reflexive transitive antisymmetric upper-bounded up-complete /\-complete -> non empty complete for RelStr ; correctness coherence for b1 being non empty Poset st b1 is up-complete & b1 is /\-complete & b1 is upper-bounded holds b1 is complete ; ; end; theorem Th29: :: YELLOW_2:29 for L being complete LATTICE for f being Function of L,L st f is monotone holds for M being Subset of L st M = { x where x is Element of L : x = f . x } holds subrelstr M is complete LATTICE proof let L be complete LATTICE; ::_thesis: for f being Function of L,L st f is monotone holds for M being Subset of L st M = { x where x is Element of L : x = f . x } holds subrelstr M is complete LATTICE let f be Function of L,L; ::_thesis: ( f is monotone implies for M being Subset of L st M = { x where x is Element of L : x = f . x } holds subrelstr M is complete LATTICE ) assume A1: f is monotone ; ::_thesis: for M being Subset of L st M = { x where x is Element of L : x = f . x } holds subrelstr M is complete LATTICE let M be Subset of L; ::_thesis: ( M = { x where x is Element of L : x = f . x } implies subrelstr M is complete LATTICE ) assume A2: M = { x where x is Element of L : x = f . x } ; ::_thesis: subrelstr M is complete LATTICE set S = subrelstr M; A3: for X being Subset of (subrelstr M) for Y being Subset of L st Y = { y where y is Element of L : ( X is_<=_than f . y & f . y <= y ) } holds inf Y in M proof let X be Subset of (subrelstr M); ::_thesis: for Y being Subset of L st Y = { y where y is Element of L : ( X is_<=_than f . y & f . y <= y ) } holds inf Y in M let Y be Subset of L; ::_thesis: ( Y = { y where y is Element of L : ( X is_<=_than f . y & f . y <= y ) } implies inf Y in M ) assume A4: Y = { y where y is Element of L : ( X is_<=_than f . y & f . y <= y ) } ; ::_thesis: inf Y in M set z = inf Y; A5: f . (inf Y) is_<=_than Y proof let u be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not u in Y or f . (inf Y) <= u ) assume A6: u in Y ; ::_thesis: f . (inf Y) <= u then consider y being Element of L such that A7: y = u and X is_<=_than f . y and A8: f . y <= y by A4; inf Y <= u by A6, Th22; then f . (inf Y) <= f . y by A1, A7, ORDERS_3:def_5; hence f . (inf Y) <= u by A7, A8, ORDERS_2:3; ::_thesis: verum end; A9: X is_<=_than f . (f . (inf Y)) proof let m be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not m in X or m <= f . (f . (inf Y)) ) assume A10: m in X ; ::_thesis: m <= f . (f . (inf Y)) m is_<=_than Y proof let u be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not u in Y or m <= u ) assume u in Y ; ::_thesis: m <= u then consider y being Element of L such that A11: y = u and A12: X is_<=_than f . y and A13: f . y <= y by A4; m <= f . y by A10, A12, LATTICE3:def_9; hence m <= u by A11, A13, ORDERS_2:3; ::_thesis: verum end; then m <= inf Y by YELLOW_0:33; then A14: f . m <= f . (inf Y) by A1, ORDERS_3:def_5; X c= the carrier of (subrelstr M) ; then X c= M by YELLOW_0:def_15; then m in M by A10; then ex x being Element of L st ( x = m & x = f . x ) by A2; hence m <= f . (f . (inf Y)) by A1, A14, ORDERS_3:def_5; ::_thesis: verum end; ex_inf_of Y,L by YELLOW_0:17; then A15: f . (inf Y) <= inf Y by A5, YELLOW_0:31; then f . (f . (inf Y)) <= f . (inf Y) by A1, ORDERS_3:def_5; then f . (inf Y) in Y by A4, A9; then inf Y <= f . (inf Y) by Th22; then inf Y = f . (inf Y) by A15, ORDERS_2:2; hence inf Y in M by A2; ::_thesis: verum end; M c= the carrier of (subrelstr M) by YELLOW_0:def_15; then reconsider M = M as Subset of (subrelstr M) ; defpred S1[ Element of L] means ( M is_<=_than f . $1 & f . $1 <= $1 ); reconsider Y = { y where y is Element of L : S1[y] } as Subset of L from DOMAIN_1:sch_7(); inf Y in M by A3; then reconsider S = subrelstr M as non empty Poset ; for X being Subset of S holds ex_sup_of X,S proof let X be Subset of S; ::_thesis: ex_sup_of X,S defpred S2[ Element of L] means ( X is_<=_than f . $1 & f . $1 <= $1 ); reconsider Y = { y where y is Element of L : S2[y] } as Subset of L from DOMAIN_1:sch_7(); set z = inf Y; inf Y in M by A3; then reconsider z = inf Y as Element of S ; A16: X is_<=_than z proof let x be Element of S; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= z ) x in the carrier of S ; then x in M by YELLOW_0:def_15; then consider m being Element of L such that A17: x = m and m = f . m by A2; assume A18: x in X ; ::_thesis: x <= z m is_<=_than Y proof let u be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not u in Y or m <= u ) assume u in Y ; ::_thesis: m <= u then consider y being Element of L such that A19: y = u and A20: X is_<=_than f . y and A21: f . y <= y ; m <= f . y by A18, A17, A20, LATTICE3:def_9; hence m <= u by A19, A21, ORDERS_2:3; ::_thesis: verum end; then m <= inf Y by YELLOW_0:33; hence x <= z by A17, YELLOW_0:60; ::_thesis: verum end; for b being Element of S st X is_<=_than b holds z <= b proof let b be Element of S; ::_thesis: ( X is_<=_than b implies z <= b ) b in the carrier of S ; then b in M by YELLOW_0:def_15; then consider x being Element of L such that A22: x = b and A23: x = f . x by A2; assume X is_<=_than b ; ::_thesis: z <= b then X is_<=_than f . x by A22, A23, YELLOW_0:62; then x in Y by A23; hence z <= b by A22, Th22, YELLOW_0:60; ::_thesis: verum end; hence ex_sup_of X,S by A16, YELLOW_0:30; ::_thesis: verum end; then reconsider S = S as non empty complete Poset by YELLOW_0:53; S is complete LATTICE ; hence subrelstr M is complete LATTICE ; ::_thesis: verum end; theorem Th30: :: YELLOW_2:30 for L being complete LATTICE for S being non empty full infs-inheriting SubRelStr of L holds S is complete LATTICE proof let L be complete LATTICE; ::_thesis: for S being non empty full infs-inheriting SubRelStr of L holds S is complete LATTICE let S be non empty full infs-inheriting SubRelStr of L; ::_thesis: S is complete LATTICE for X being Subset of S holds ex_inf_of X,S proof let X be Subset of S; ::_thesis: ex_inf_of X,S A1: ex_inf_of X,L by YELLOW_0:17; then "/\" (X,L) in the carrier of S by YELLOW_0:def_18; hence ex_inf_of X,S by A1, YELLOW_0:63; ::_thesis: verum end; then S is complete by Th28; hence S is complete LATTICE ; ::_thesis: verum end; theorem Th31: :: YELLOW_2:31 for L being complete LATTICE for S being non empty full sups-inheriting SubRelStr of L holds S is complete LATTICE proof let L be complete LATTICE; ::_thesis: for S being non empty full sups-inheriting SubRelStr of L holds S is complete LATTICE let S be non empty full sups-inheriting SubRelStr of L; ::_thesis: S is complete LATTICE for X being Subset of S holds ex_sup_of X,S proof let X be Subset of S; ::_thesis: ex_sup_of X,S A1: ex_sup_of X,L by YELLOW_0:17; then "\/" (X,L) in the carrier of S by YELLOW_0:def_19; hence ex_sup_of X,S by A1, YELLOW_0:64; ::_thesis: verum end; then S is complete by YELLOW_0:53; hence S is complete LATTICE ; ::_thesis: verum end; theorem Th32: :: YELLOW_2:32 for L being complete LATTICE for M being non empty RelStr for f being Function of L,M st f is sups-preserving holds Image f is sups-inheriting proof let L be complete LATTICE; ::_thesis: for M being non empty RelStr for f being Function of L,M st f is sups-preserving holds Image f is sups-inheriting let M be non empty RelStr ; ::_thesis: for f being Function of L,M st f is sups-preserving holds Image f is sups-inheriting let f be Function of L,M; ::_thesis: ( f is sups-preserving implies Image f is sups-inheriting ) assume A1: f is sups-preserving ; ::_thesis: Image f is sups-inheriting set S = subrelstr (rng f); for Y being Subset of (subrelstr (rng f)) st ex_sup_of Y,M holds "\/" (Y,M) in the carrier of (subrelstr (rng f)) proof let Y be Subset of (subrelstr (rng f)); ::_thesis: ( ex_sup_of Y,M implies "\/" (Y,M) in the carrier of (subrelstr (rng f)) ) assume ex_sup_of Y,M ; ::_thesis: "\/" (Y,M) in the carrier of (subrelstr (rng f)) A2: ( f preserves_sup_of f " Y & ex_sup_of f " Y,L ) by A1, WAYBEL_0:def_33, YELLOW_0:17; Y c= the carrier of (subrelstr (rng f)) ; then Y c= rng f by YELLOW_0:def_15; then "\/" (Y,M) = sup (f .: (f " Y)) by FUNCT_1:77 .= f . (sup (f " Y)) by A2, WAYBEL_0:def_31 ; then "\/" (Y,M) in rng f by FUNCT_2:4; hence "\/" (Y,M) in the carrier of (subrelstr (rng f)) by YELLOW_0:def_15; ::_thesis: verum end; hence Image f is sups-inheriting by YELLOW_0:def_19; ::_thesis: verum end; theorem Th33: :: YELLOW_2:33 for L being complete LATTICE for M being non empty RelStr for f being Function of L,M st f is infs-preserving holds Image f is infs-inheriting proof let L be complete LATTICE; ::_thesis: for M being non empty RelStr for f being Function of L,M st f is infs-preserving holds Image f is infs-inheriting let M be non empty RelStr ; ::_thesis: for f being Function of L,M st f is infs-preserving holds Image f is infs-inheriting let f be Function of L,M; ::_thesis: ( f is infs-preserving implies Image f is infs-inheriting ) assume A1: f is infs-preserving ; ::_thesis: Image f is infs-inheriting set S = subrelstr (rng f); for Y being Subset of (subrelstr (rng f)) st ex_inf_of Y,M holds "/\" (Y,M) in the carrier of (subrelstr (rng f)) proof let Y be Subset of (subrelstr (rng f)); ::_thesis: ( ex_inf_of Y,M implies "/\" (Y,M) in the carrier of (subrelstr (rng f)) ) assume ex_inf_of Y,M ; ::_thesis: "/\" (Y,M) in the carrier of (subrelstr (rng f)) A2: ( f preserves_inf_of f " Y & ex_inf_of f " Y,L ) by A1, WAYBEL_0:def_32, YELLOW_0:17; Y c= the carrier of (subrelstr (rng f)) ; then Y c= rng f by YELLOW_0:def_15; then "/\" (Y,M) = inf (f .: (f " Y)) by FUNCT_1:77 .= f . (inf (f " Y)) by A2, WAYBEL_0:def_30 ; then "/\" (Y,M) in rng f by FUNCT_2:4; hence "/\" (Y,M) in the carrier of (subrelstr (rng f)) by YELLOW_0:def_15; ::_thesis: verum end; hence Image f is infs-inheriting by YELLOW_0:def_18; ::_thesis: verum end; theorem :: YELLOW_2:34 for L, M being complete LATTICE for f being Function of L,M st ( f is sups-preserving or f is infs-preserving ) holds Image f is complete LATTICE proof let L, M be complete LATTICE; ::_thesis: for f being Function of L,M st ( f is sups-preserving or f is infs-preserving ) holds Image f is complete LATTICE let f be Function of L,M; ::_thesis: ( ( f is sups-preserving or f is infs-preserving ) implies Image f is complete LATTICE ) assume A1: ( f is sups-preserving or f is infs-preserving ) ; ::_thesis: Image f is complete LATTICE percases ( f is sups-preserving or f is infs-preserving ) by A1; suppose f is sups-preserving ; ::_thesis: Image f is complete LATTICE then Image f is sups-inheriting by Th32; hence Image f is complete LATTICE by Th31; ::_thesis: verum end; suppose f is infs-preserving ; ::_thesis: Image f is complete LATTICE then Image f is infs-inheriting by Th33; hence Image f is complete LATTICE by Th30; ::_thesis: verum end; end; end; theorem :: YELLOW_2:35 for L being complete LATTICE for f being Function of L,L st f is idempotent & f is directed-sups-preserving holds ( Image f is directed-sups-inheriting & Image f is complete LATTICE ) proof let L be complete LATTICE; ::_thesis: for f being Function of L,L st f is idempotent & f is directed-sups-preserving holds ( Image f is directed-sups-inheriting & Image f is complete LATTICE ) let f be Function of L,L; ::_thesis: ( f is idempotent & f is directed-sups-preserving implies ( Image f is directed-sups-inheriting & Image f is complete LATTICE ) ) set S = subrelstr (rng f); set a = the Element of L; dom f = the carrier of L by FUNCT_2:def_1; then f . the Element of L in rng f by FUNCT_1:def_3; then reconsider S9 = subrelstr (rng f) as non empty full SubRelStr of L ; assume A1: ( f is idempotent & f is directed-sups-preserving ) ; ::_thesis: ( Image f is directed-sups-inheriting & Image f is complete LATTICE ) for X being directed Subset of (subrelstr (rng f)) st X <> {} & ex_sup_of X,L holds "\/" (X,L) in the carrier of (subrelstr (rng f)) proof let X be directed Subset of (subrelstr (rng f)); ::_thesis: ( X <> {} & ex_sup_of X,L implies "\/" (X,L) in the carrier of (subrelstr (rng f)) ) X c= the carrier of (subrelstr (rng f)) ; then A2: X c= rng f by YELLOW_0:def_15; assume X <> {} ; ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr (rng f)) ) then X is non empty directed Subset of S9 ; then reconsider X9 = X as non empty directed Subset of L by Th7; assume A3: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (subrelstr (rng f)) f preserves_sup_of X9 by A1, WAYBEL_0:def_37; then sup (f .: X9) = f . (sup X9) by A3, WAYBEL_0:def_31; then sup X9 = f . (sup X9) by A1, A2, Th20; then "\/" (X,L) in rng f by FUNCT_2:4; hence "\/" (X,L) in the carrier of (subrelstr (rng f)) by YELLOW_0:def_15; ::_thesis: verum end; hence Image f is directed-sups-inheriting by WAYBEL_0:def_4; ::_thesis: Image f is complete LATTICE rng f = { x where x is Element of L : x = f . x } by A1, Th19; hence Image f is complete LATTICE by A1, Th16, Th29; ::_thesis: verum end; begin theorem Th36: :: YELLOW_2:36 for L being RelStr for F being Subset-Family of L st ( for X being Subset of L st X in F holds X is lower ) holds meet F is lower Subset of L proof let L be RelStr ; ::_thesis: for F being Subset-Family of L st ( for X being Subset of L st X in F holds X is lower ) holds meet F is lower Subset of L let F be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in F holds X is lower ) implies meet F is lower Subset of L ) reconsider F9 = F as Subset-Family of L ; assume A1: for X being Subset of L st X in F holds X is lower ; ::_thesis: meet F is lower Subset of L reconsider M = meet F9 as Subset of L ; percases ( F = {} or F <> {} ) ; suppose F = {} ; ::_thesis: meet F is lower Subset of L then for x, y being Element of L st x in M & y <= x holds y in M by SETFAM_1:def_1; hence meet F is lower Subset of L by WAYBEL_0:def_19; ::_thesis: verum end; supposeA2: F <> {} ; ::_thesis: meet F is lower Subset of L for x, y being Element of L st x in M & y <= x holds y in M proof let x, y be Element of L; ::_thesis: ( x in M & y <= x implies y in M ) assume that A3: x in M and A4: y <= x ; ::_thesis: y in M for Y being set st Y in F holds y in Y proof let Y be set ; ::_thesis: ( Y in F implies y in Y ) assume A5: Y in F ; ::_thesis: y in Y then reconsider X = Y as Subset of L ; ( X is lower & x in X ) by A1, A3, A5, SETFAM_1:def_1; hence y in Y by A4, WAYBEL_0:def_19; ::_thesis: verum end; hence y in M by A2, SETFAM_1:def_1; ::_thesis: verum end; hence meet F is lower Subset of L by WAYBEL_0:def_19; ::_thesis: verum end; end; end; theorem :: YELLOW_2:37 for L being RelStr for F being Subset-Family of L st ( for X being Subset of L st X in F holds X is upper ) holds meet F is upper Subset of L proof let L be RelStr ; ::_thesis: for F being Subset-Family of L st ( for X being Subset of L st X in F holds X is upper ) holds meet F is upper Subset of L let F be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in F holds X is upper ) implies meet F is upper Subset of L ) reconsider F9 = F as Subset-Family of L ; assume A1: for X being Subset of L st X in F holds X is upper ; ::_thesis: meet F is upper Subset of L reconsider M = meet F9 as Subset of L ; percases ( F = {} or F <> {} ) ; suppose F = {} ; ::_thesis: meet F is upper Subset of L then for x, y being Element of L st x in M & x <= y holds y in M by SETFAM_1:def_1; hence meet F is upper Subset of L by WAYBEL_0:def_20; ::_thesis: verum end; supposeA2: F <> {} ; ::_thesis: meet F is upper Subset of L for x, y being Element of L st x in M & x <= y holds y in M proof let x, y be Element of L; ::_thesis: ( x in M & x <= y implies y in M ) assume that A3: x in M and A4: x <= y ; ::_thesis: y in M for Y being set st Y in F holds y in Y proof let Y be set ; ::_thesis: ( Y in F implies y in Y ) assume A5: Y in F ; ::_thesis: y in Y then reconsider X = Y as Subset of L ; ( X is upper & x in X ) by A1, A3, A5, SETFAM_1:def_1; hence y in Y by A4, WAYBEL_0:def_20; ::_thesis: verum end; hence y in M by A2, SETFAM_1:def_1; ::_thesis: verum end; hence meet F is upper Subset of L by WAYBEL_0:def_20; ::_thesis: verum end; end; end; theorem Th38: :: YELLOW_2:38 for L being antisymmetric with_suprema RelStr for F being Subset-Family of L st ( for X being Subset of L st X in F holds ( X is lower & X is directed ) ) holds meet F is directed Subset of L proof let L be antisymmetric with_suprema RelStr ; ::_thesis: for F being Subset-Family of L st ( for X being Subset of L st X in F holds ( X is lower & X is directed ) ) holds meet F is directed Subset of L let F be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in F holds ( X is lower & X is directed ) ) implies meet F is directed Subset of L ) assume A1: for X being Subset of L st X in F holds ( X is lower & X is directed ) ; ::_thesis: meet F is directed Subset of L reconsider F9 = F as Subset-Family of L ; reconsider M = meet F9 as Subset of L ; percases ( F = {} or F <> {} ) ; supposeA2: F = {} ; ::_thesis: meet F is directed Subset of L M is directed proof let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in M or not y in M or ex b1 being Element of the carrier of L st ( b1 in M & x <= b1 & y <= b1 ) ) assume that A3: x in M and y in M ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in M & x <= b1 & y <= b1 ) thus ex b1 being Element of the carrier of L st ( b1 in M & x <= b1 & y <= b1 ) by A2, A3, SETFAM_1:def_1; ::_thesis: verum end; hence meet F is directed Subset of L ; ::_thesis: verum end; supposeA4: F <> {} ; ::_thesis: meet F is directed Subset of L M is directed proof let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in M or not y in M or ex b1 being Element of the carrier of L st ( b1 in M & x <= b1 & y <= b1 ) ) assume that A5: x in M and A6: y in M ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in M & x <= b1 & y <= b1 ) take z = x "\/" y; ::_thesis: ( z in M & x <= z & y <= z ) for Y being set st Y in F holds z in Y proof let Y be set ; ::_thesis: ( Y in F implies z in Y ) assume A7: Y in F ; ::_thesis: z in Y then reconsider X = Y as Subset of L ; A8: y in X by A6, A7, SETFAM_1:def_1; ( X is lower & X is directed & x in X ) by A1, A5, A7, SETFAM_1:def_1; hence z in Y by A8, WAYBEL_0:40; ::_thesis: verum end; hence z in M by A4, SETFAM_1:def_1; ::_thesis: ( x <= z & y <= z ) thus ( x <= z & y <= z ) by YELLOW_0:22; ::_thesis: verum end; hence meet F is directed Subset of L ; ::_thesis: verum end; end; end; theorem :: YELLOW_2:39 for L being antisymmetric with_infima RelStr for F being Subset-Family of L st ( for X being Subset of L st X in F holds ( X is upper & X is filtered ) ) holds meet F is filtered Subset of L proof let L be antisymmetric with_infima RelStr ; ::_thesis: for F being Subset-Family of L st ( for X being Subset of L st X in F holds ( X is upper & X is filtered ) ) holds meet F is filtered Subset of L let F be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in F holds ( X is upper & X is filtered ) ) implies meet F is filtered Subset of L ) assume A1: for X being Subset of L st X in F holds ( X is upper & X is filtered ) ; ::_thesis: meet F is filtered Subset of L reconsider F9 = F as Subset-Family of L ; reconsider M = meet F9 as Subset of L ; percases ( F = {} or F <> {} ) ; supposeA2: F = {} ; ::_thesis: meet F is filtered Subset of L M is filtered proof let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in M or not y in M or ex b1 being Element of the carrier of L st ( b1 in M & b1 <= x & b1 <= y ) ) assume that A3: x in M and y in M ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in M & b1 <= x & b1 <= y ) thus ex b1 being Element of the carrier of L st ( b1 in M & b1 <= x & b1 <= y ) by A2, A3, SETFAM_1:def_1; ::_thesis: verum end; hence meet F is filtered Subset of L ; ::_thesis: verum end; supposeA4: F <> {} ; ::_thesis: meet F is filtered Subset of L M is filtered proof let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in M or not y in M or ex b1 being Element of the carrier of L st ( b1 in M & b1 <= x & b1 <= y ) ) assume that A5: x in M and A6: y in M ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in M & b1 <= x & b1 <= y ) take z = x "/\" y; ::_thesis: ( z in M & z <= x & z <= y ) for Y being set st Y in F holds z in Y proof let Y be set ; ::_thesis: ( Y in F implies z in Y ) assume A7: Y in F ; ::_thesis: z in Y then reconsider X = Y as Subset of L ; A8: y in X by A6, A7, SETFAM_1:def_1; ( X is upper & X is filtered & x in X ) by A1, A5, A7, SETFAM_1:def_1; hence z in Y by A8, WAYBEL_0:41; ::_thesis: verum end; hence z in M by A4, SETFAM_1:def_1; ::_thesis: ( z <= x & z <= y ) thus ( z <= x & z <= y ) by YELLOW_0:23; ::_thesis: verum end; hence meet F is filtered Subset of L ; ::_thesis: verum end; end; end; theorem Th40: :: YELLOW_2:40 for L being with_infima Poset for I, J being Ideal of L holds I /\ J is Ideal of L proof let L be with_infima Poset; ::_thesis: for I, J being Ideal of L holds I /\ J is Ideal of L let I, J be Ideal of L; ::_thesis: I /\ J is Ideal of L set i = the Element of I; set j = the Element of J; set a = the Element of I "/\" the Element of J; the Element of I "/\" the Element of J <= the Element of J by YELLOW_0:23; then A1: the Element of I "/\" the Element of J in J by WAYBEL_0:def_19; the Element of I "/\" the Element of J <= the Element of I by YELLOW_0:23; then the Element of I "/\" the Element of J in I by WAYBEL_0:def_19; hence I /\ J is Ideal of L by A1, WAYBEL_0:27, WAYBEL_0:44, XBOOLE_0:def_4; ::_thesis: verum end; registration let L be non empty reflexive transitive RelStr ; cluster Ids L -> non empty ; correctness coherence not Ids L is empty ; proof set x = the Element of L; downarrow the Element of L in { Y where Y is Ideal of L : verum } ; hence not Ids L is empty ; ::_thesis: verum end; end; theorem Th41: :: YELLOW_2:41 for x being set for L being non empty reflexive transitive RelStr holds ( x is Element of (InclPoset (Ids L)) iff x is Ideal of L ) proof let x be set ; ::_thesis: for L being non empty reflexive transitive RelStr holds ( x is Element of (InclPoset (Ids L)) iff x is Ideal of L ) let L be non empty reflexive transitive RelStr ; ::_thesis: ( x is Element of (InclPoset (Ids L)) iff x is Ideal of L ) hereby ::_thesis: ( x is Ideal of L implies x is Element of (InclPoset (Ids L)) ) assume x is Element of (InclPoset (Ids L)) ; ::_thesis: x is Ideal of L then x in the carrier of (InclPoset (Ids L)) ; then x in Ids L by YELLOW_1:1; then ex J being Ideal of L st J = x ; hence x is Ideal of L ; ::_thesis: verum end; assume x is Ideal of L ; ::_thesis: x is Element of (InclPoset (Ids L)) then x in { Y where Y is Ideal of L : verum } ; hence x is Element of (InclPoset (Ids L)) by YELLOW_1:1; ::_thesis: verum end; theorem Th42: :: YELLOW_2:42 for x being set for L being non empty reflexive transitive RelStr for I being Element of (InclPoset (Ids L)) st x in I holds x is Element of L proof let x be set ; ::_thesis: for L being non empty reflexive transitive RelStr for I being Element of (InclPoset (Ids L)) st x in I holds x is Element of L let L be non empty reflexive transitive RelStr ; ::_thesis: for I being Element of (InclPoset (Ids L)) st x in I holds x is Element of L let I be Element of (InclPoset (Ids L)); ::_thesis: ( x in I implies x is Element of L ) reconsider I9 = I as non empty Subset of L by Th41; assume x in I ; ::_thesis: x is Element of L then reconsider x9 = x as Element of I9 ; x9 in the carrier of L ; hence x is Element of L ; ::_thesis: verum end; theorem :: YELLOW_2:43 for L being with_infima Poset for x, y being Element of (InclPoset (Ids L)) holds x "/\" y = x /\ y proof let L be with_infima Poset; ::_thesis: for x, y being Element of (InclPoset (Ids L)) holds x "/\" y = x /\ y let x, y be Element of (InclPoset (Ids L)); ::_thesis: x "/\" y = x /\ y reconsider x9 = x, y9 = y as Ideal of L by Th41; x9 /\ y9 is Ideal of L by Th40; then x9 /\ y9 in { X where X is Ideal of L : verum } ; hence x "/\" y = x /\ y by YELLOW_1:9; ::_thesis: verum end; registration let L be with_infima Poset; cluster InclPoset (Ids L) -> with_infima ; correctness coherence InclPoset (Ids L) is with_infima ; proof for x, y being set st x in Ids L & y in Ids L holds x /\ y in Ids L proof let x, y be set ; ::_thesis: ( x in Ids L & y in Ids L implies x /\ y in Ids L ) assume that A1: x in Ids L and A2: y in Ids L ; ::_thesis: x /\ y in Ids L consider I being Ideal of L such that A3: I = x by A1; consider J being Ideal of L such that A4: J = y by A2; I /\ J is Ideal of L by Th40; hence x /\ y in Ids L by A3, A4; ::_thesis: verum end; hence InclPoset (Ids L) is with_infima by YELLOW_1:12; ::_thesis: verum end; end; theorem Th44: :: YELLOW_2:44 for L being with_suprema Poset for x, y being Element of (InclPoset (Ids L)) ex Z being Subset of L st ( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st ( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z ) proof let L be with_suprema Poset; ::_thesis: for x, y being Element of (InclPoset (Ids L)) ex Z being Subset of L st ( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st ( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z ) set P = InclPoset (Ids L); let x, y be Element of (InclPoset (Ids L)); ::_thesis: ex Z being Subset of L st ( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st ( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z ) defpred S1[ Element of L] means ( $1 in x or $1 in y or ex a, b being Element of L st ( a in x & b in y & $1 = a "\/" b ) ); reconsider Z = { z where z is Element of L : S1[z] } as Subset of L from DOMAIN_1:sch_7(); take Z ; ::_thesis: ( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st ( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z ) reconsider x9 = x, y9 = y as Ideal of L by Th41; set z = the Element of x9; the Element of x9 in Z ; then reconsider Z = Z as non empty Subset of L ; set DZ = downarrow Z; for u, v being Element of L st u in Z & v in Z holds ex z being Element of L st ( z in Z & u <= z & v <= z ) proof A1: for p, q being Element of L st p in y & ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) holds ex z being Element of L st ( z in Z & p <= z & q <= z ) proof let p, q be Element of L; ::_thesis: ( p in y & ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) implies ex z being Element of L st ( z in Z & p <= z & q <= z ) ) assume that A2: p in y and A3: ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) ; ::_thesis: ex z being Element of L st ( z in Z & p <= z & q <= z ) consider a, b being Element of L such that A4: a in x and A5: b in y and A6: q = a "\/" b by A3; reconsider c = b "\/" p as Element of L ; take z = a "\/" c; ::_thesis: ( z in Z & p <= z & q <= z ) c in y9 by A2, A5, WAYBEL_0:40; hence z in Z by A4; ::_thesis: ( p <= z & q <= z ) A7: c <= z by YELLOW_0:22; A8: ( p <= c & a <= z ) by YELLOW_0:22; b <= c by YELLOW_0:22; then b <= z by A7, ORDERS_2:3; hence ( p <= z & q <= z ) by A6, A7, A8, ORDERS_2:3, YELLOW_0:22; ::_thesis: verum end; A9: for p, q being Element of L st p in x & ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) holds ex z being Element of L st ( z in Z & p <= z & q <= z ) proof let p, q be Element of L; ::_thesis: ( p in x & ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) implies ex z being Element of L st ( z in Z & p <= z & q <= z ) ) assume that A10: p in x and A11: ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) ; ::_thesis: ex z being Element of L st ( z in Z & p <= z & q <= z ) consider a, b being Element of L such that A12: a in x and A13: b in y and A14: q = a "\/" b by A11; reconsider c = a "\/" p as Element of L ; take z = c "\/" b; ::_thesis: ( z in Z & p <= z & q <= z ) c in x9 by A10, A12, WAYBEL_0:40; hence z in Z by A13; ::_thesis: ( p <= z & q <= z ) A15: c <= z by YELLOW_0:22; A16: ( p <= c & b <= z ) by YELLOW_0:22; a <= c by YELLOW_0:22; then a <= z by A15, ORDERS_2:3; hence ( p <= z & q <= z ) by A14, A15, A16, ORDERS_2:3, YELLOW_0:22; ::_thesis: verum end; let u, v be Element of L; ::_thesis: ( u in Z & v in Z implies ex z being Element of L st ( z in Z & u <= z & v <= z ) ) assume that A17: u in Z and A18: v in Z ; ::_thesis: ex z being Element of L st ( z in Z & u <= z & v <= z ) consider p being Element of L such that A19: p = u and A20: ( p in x or p in y or ex a, b being Element of L st ( a in x & b in y & p = a "\/" b ) ) by A17; consider q being Element of L such that A21: q = v and A22: ( q in x or q in y or ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) ) by A18; percases ( ( p in x & q in x ) or ( p in x & q in y ) or ( p in x & ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) ) or ( p in y & q in x ) or ( p in y & q in y ) or ( p in y & ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) ) or ( q in x & ex a, b being Element of L st ( a in x & b in y & p = a "\/" b ) ) or ( q in y & ex a, b being Element of L st ( a in x & b in y & p = a "\/" b ) ) or ( ex a, b being Element of L st ( a in x & b in y & p = a "\/" b ) & ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) ) ) by A20, A22; suppose ( p in x & q in x ) ; ::_thesis: ex z being Element of L st ( z in Z & u <= z & v <= z ) then consider z being Element of L such that A23: ( z in x9 & p <= z & q <= z ) by WAYBEL_0:def_1; take z ; ::_thesis: ( z in Z & u <= z & v <= z ) thus ( z in Z & u <= z & v <= z ) by A19, A21, A23; ::_thesis: verum end; supposeA24: ( p in x & q in y ) ; ::_thesis: ex z being Element of L st ( z in Z & u <= z & v <= z ) take p "\/" q ; ::_thesis: ( p "\/" q in Z & u <= p "\/" q & v <= p "\/" q ) thus ( p "\/" q in Z & u <= p "\/" q & v <= p "\/" q ) by A19, A21, A24, YELLOW_0:22; ::_thesis: verum end; suppose ( p in x & ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) ) ; ::_thesis: ex z being Element of L st ( z in Z & u <= z & v <= z ) then consider z being Element of L such that A25: ( z in Z & p <= z & q <= z ) by A9; take z ; ::_thesis: ( z in Z & u <= z & v <= z ) thus ( z in Z & u <= z & v <= z ) by A19, A21, A25; ::_thesis: verum end; supposeA26: ( p in y & q in x ) ; ::_thesis: ex z being Element of L st ( z in Z & u <= z & v <= z ) take q "\/" p ; ::_thesis: ( q "\/" p in Z & u <= q "\/" p & v <= q "\/" p ) thus ( q "\/" p in Z & u <= q "\/" p & v <= q "\/" p ) by A19, A21, A26, YELLOW_0:22; ::_thesis: verum end; suppose ( p in y & q in y ) ; ::_thesis: ex z being Element of L st ( z in Z & u <= z & v <= z ) then consider z being Element of L such that A27: ( z in y9 & p <= z & q <= z ) by WAYBEL_0:def_1; take z ; ::_thesis: ( z in Z & u <= z & v <= z ) thus ( z in Z & u <= z & v <= z ) by A19, A21, A27; ::_thesis: verum end; suppose ( p in y & ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) ) ; ::_thesis: ex z being Element of L st ( z in Z & u <= z & v <= z ) then consider z being Element of L such that A28: ( z in Z & p <= z & q <= z ) by A1; take z ; ::_thesis: ( z in Z & u <= z & v <= z ) thus ( z in Z & u <= z & v <= z ) by A19, A21, A28; ::_thesis: verum end; suppose ( q in x & ex a, b being Element of L st ( a in x & b in y & p = a "\/" b ) ) ; ::_thesis: ex z being Element of L st ( z in Z & u <= z & v <= z ) then consider z being Element of L such that A29: ( z in Z & q <= z & p <= z ) by A9; take z ; ::_thesis: ( z in Z & u <= z & v <= z ) thus ( z in Z & u <= z & v <= z ) by A19, A21, A29; ::_thesis: verum end; suppose ( q in y & ex a, b being Element of L st ( a in x & b in y & p = a "\/" b ) ) ; ::_thesis: ex z being Element of L st ( z in Z & u <= z & v <= z ) then consider z being Element of L such that A30: ( z in Z & q <= z & p <= z ) by A1; take z ; ::_thesis: ( z in Z & u <= z & v <= z ) thus ( z in Z & u <= z & v <= z ) by A19, A21, A30; ::_thesis: verum end; suppose ( ex a, b being Element of L st ( a in x & b in y & p = a "\/" b ) & ex a, b being Element of L st ( a in x & b in y & q = a "\/" b ) ) ; ::_thesis: ex z being Element of L st ( z in Z & u <= z & v <= z ) then consider a, b, c, d being Element of L such that A31: ( a in x & b in y ) and A32: p = a "\/" b and A33: ( c in x & d in y ) and A34: q = c "\/" d ; reconsider ac = a "\/" c, bd = b "\/" d as Element of L ; take z = ac "\/" bd; ::_thesis: ( z in Z & u <= z & v <= z ) ( ac in x9 & bd in y9 ) by A31, A33, WAYBEL_0:40; hence z in Z ; ::_thesis: ( u <= z & v <= z ) A35: ac <= z by YELLOW_0:22; A36: bd <= z by YELLOW_0:22; b <= bd by YELLOW_0:22; then A37: b <= z by A36, ORDERS_2:3; a <= ac by YELLOW_0:22; then a <= z by A35, ORDERS_2:3; hence u <= z by A19, A32, A37, YELLOW_0:22; ::_thesis: v <= z d <= bd by YELLOW_0:22; then A38: d <= z by A36, ORDERS_2:3; c <= ac by YELLOW_0:22; then c <= z by A35, ORDERS_2:3; hence v <= z by A21, A34, A38, YELLOW_0:22; ::_thesis: verum end; end; end; then Z is directed by WAYBEL_0:def_1; then reconsider DZ = downarrow Z as Element of (InclPoset (Ids L)) by Th41; A39: for d being Element of (InclPoset (Ids L)) st d >= x & d >= y holds DZ <= d proof let d be Element of (InclPoset (Ids L)); ::_thesis: ( d >= x & d >= y implies DZ <= d ) assume that A40: x <= d and A41: y <= d ; ::_thesis: DZ <= d A42: y c= d by A41, YELLOW_1:3; A43: x c= d by A40, YELLOW_1:3; DZ c= d proof let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in DZ or p in d ) assume p in DZ ; ::_thesis: p in d then p in { q where q is Element of L : ex u being Element of L st ( q <= u & u in Z ) } by WAYBEL_0:14; then consider p9 being Element of L such that A44: p9 = p and A45: ex u being Element of L st ( p9 <= u & u in Z ) ; consider u being Element of L such that A46: p9 <= u and A47: u in Z by A45; consider z being Element of L such that A48: z = u and A49: ( z in x or z in y or ex a, b being Element of L st ( a in x & b in y & z = a "\/" b ) ) by A47; percases ( z in x or z in y or ex a, b being Element of L st ( a in x & b in y & z = a "\/" b ) ) by A49; suppose z in x ; ::_thesis: p in d then p in x9 by A44, A46, A48, WAYBEL_0:def_19; hence p in d by A43; ::_thesis: verum end; suppose z in y ; ::_thesis: p in d then p in y9 by A44, A46, A48, WAYBEL_0:def_19; hence p in d by A42; ::_thesis: verum end; supposeA50: ex a, b being Element of L st ( a in x & b in y & z = a "\/" b ) ; ::_thesis: p in d reconsider d9 = d as Ideal of L by Th41; u in d9 by A43, A42, A48, A50, WAYBEL_0:40; hence p in d by A44, A46, WAYBEL_0:def_19; ::_thesis: verum end; end; end; hence DZ <= d by YELLOW_1:3; ::_thesis: verum end; y c= DZ proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in y or a in DZ ) A51: Z c= DZ by WAYBEL_0:16; assume A52: a in y ; ::_thesis: a in DZ then reconsider a9 = a as Element of L by Th42; a9 in Z by A52; hence a in DZ by A51; ::_thesis: verum end; then A53: y <= DZ by YELLOW_1:3; x c= DZ proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in DZ ) A54: Z c= DZ by WAYBEL_0:16; assume A55: a in x ; ::_thesis: a in DZ then reconsider a9 = a as Element of L by Th42; a9 in Z by A55; hence a in DZ by A54; ::_thesis: verum end; then x <= DZ by YELLOW_1:3; hence ( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st ( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z ) by A53, A39, YELLOW_0:18; ::_thesis: verum end; registration let L be with_suprema Poset; cluster InclPoset (Ids L) -> with_suprema ; correctness coherence InclPoset (Ids L) is with_suprema ; proof set P = InclPoset (Ids L); for x, y being Element of (InclPoset (Ids L)) ex z being Element of (InclPoset (Ids L)) st ( x <= z & y <= z & ( for z9 being Element of (InclPoset (Ids L)) st x <= z9 & y <= z9 holds z <= z9 ) ) proof let x, y be Element of (InclPoset (Ids L)); ::_thesis: ex z being Element of (InclPoset (Ids L)) st ( x <= z & y <= z & ( for z9 being Element of (InclPoset (Ids L)) st x <= z9 & y <= z9 holds z <= z9 ) ) take x "\/" y ; ::_thesis: ( x <= x "\/" y & y <= x "\/" y & ( for z9 being Element of (InclPoset (Ids L)) st x <= z9 & y <= z9 holds x "\/" y <= z9 ) ) ex Z being Subset of L st ( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st ( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z ) by Th44; hence ( x <= x "\/" y & y <= x "\/" y & ( for z9 being Element of (InclPoset (Ids L)) st x <= z9 & y <= z9 holds x "\/" y <= z9 ) ) by YELLOW_0:18; ::_thesis: verum end; hence InclPoset (Ids L) is with_suprema by LATTICE3:def_10; ::_thesis: verum end; end; theorem Th45: :: YELLOW_2:45 for L being lower-bounded sup-Semilattice for X being non empty Subset of (Ids L) holds meet X is Ideal of L proof let L be lower-bounded sup-Semilattice; ::_thesis: for X being non empty Subset of (Ids L) holds meet X is Ideal of L let X be non empty Subset of (Ids L); ::_thesis: meet X is Ideal of L A1: for J being set st J in X holds J is Ideal of L proof let J be set ; ::_thesis: ( J in X implies J is Ideal of L ) assume J in X ; ::_thesis: J is Ideal of L then J in Ids L ; then ex Y being Ideal of L st Y = J ; hence J is Ideal of L ; ::_thesis: verum end; X c= bool the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in bool the carrier of L ) assume x in X ; ::_thesis: x in bool the carrier of L then x is Ideal of L by A1; hence x in bool the carrier of L ; ::_thesis: verum end; then reconsider F = X as Subset-Family of L ; for J being Subset of L st J in F holds J is lower by A1; then reconsider I = meet X as lower Subset of L by Th36; for J being set st J in X holds Bottom L in J proof let J be set ; ::_thesis: ( J in X implies Bottom L in J ) assume J in X ; ::_thesis: Bottom L in J then reconsider J9 = J as Ideal of L by A1; set j = the Element of J9; Bottom L <= the Element of J9 by YELLOW_0:44; hence Bottom L in J by WAYBEL_0:def_19; ::_thesis: verum end; then reconsider I = I as non empty lower Subset of L by SETFAM_1:def_1; for J being Subset of L st J in F holds ( J is lower & J is directed ) by A1; then I is Ideal of L by Th38; hence meet X is Ideal of L ; ::_thesis: verum end; theorem Th46: :: YELLOW_2:46 for L being lower-bounded sup-Semilattice for A being non empty Subset of (InclPoset (Ids L)) holds ( ex_inf_of A, InclPoset (Ids L) & inf A = meet A ) proof let L be lower-bounded sup-Semilattice; ::_thesis: for A being non empty Subset of (InclPoset (Ids L)) holds ( ex_inf_of A, InclPoset (Ids L) & inf A = meet A ) let A be non empty Subset of (InclPoset (Ids L)); ::_thesis: ( ex_inf_of A, InclPoset (Ids L) & inf A = meet A ) set P = InclPoset (Ids L); reconsider A9 = A as non empty Subset of (Ids L) by YELLOW_1:1; meet A9 is Ideal of L by Th45; then reconsider I = meet A as Element of (InclPoset (Ids L)) by Th41; A1: for b being Element of (InclPoset (Ids L)) st b is_<=_than A holds I >= b proof let b be Element of (InclPoset (Ids L)); ::_thesis: ( b is_<=_than A implies I >= b ) assume A2: A is_>=_than b ; ::_thesis: I >= b A3: for J being set st J in A holds b c= J proof let J be set ; ::_thesis: ( J in A implies b c= J ) assume A4: J in A ; ::_thesis: b c= J then reconsider y = J as Element of (InclPoset (Ids L)) ; b <= y by A2, A4, LATTICE3:def_8; hence b c= J by YELLOW_1:3; ::_thesis: verum end; b c= I proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in b or c in I ) assume A5: c in b ; ::_thesis: c in I for J being set st J in A holds c in J proof let J be set ; ::_thesis: ( J in A implies c in J ) assume J in A ; ::_thesis: c in J then b c= J by A3; hence c in J by A5; ::_thesis: verum end; hence c in I by SETFAM_1:def_1; ::_thesis: verum end; hence I >= b by YELLOW_1:3; ::_thesis: verum end; I is_<=_than A proof let y be Element of (InclPoset (Ids L)); :: according to LATTICE3:def_8 ::_thesis: ( not y in A or I <= y ) assume A6: y in A ; ::_thesis: I <= y I c= y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in I or x in y ) assume x in I ; ::_thesis: x in y hence x in y by A6, SETFAM_1:def_1; ::_thesis: verum end; hence I <= y by YELLOW_1:3; ::_thesis: verum end; hence ( ex_inf_of A, InclPoset (Ids L) & inf A = meet A ) by A1, YELLOW_0:31; ::_thesis: verum end; theorem Th47: :: YELLOW_2:47 for L being with_suprema Poset holds ( ex_inf_of {} , InclPoset (Ids L) & "/\" ({},(InclPoset (Ids L))) = [#] L ) proof let L be with_suprema Poset; ::_thesis: ( ex_inf_of {} , InclPoset (Ids L) & "/\" ({},(InclPoset (Ids L))) = [#] L ) set P = InclPoset (Ids L); reconsider I = [#] L as Element of (InclPoset (Ids L)) by Th41; A1: for b being Element of (InclPoset (Ids L)) st b is_<=_than {} holds I >= b proof let b be Element of (InclPoset (Ids L)); ::_thesis: ( b is_<=_than {} implies I >= b ) reconsider b9 = b as Ideal of L by Th41; assume {} is_>=_than b ; ::_thesis: I >= b b9 c= [#] L ; hence I >= b by YELLOW_1:3; ::_thesis: verum end; I is_<=_than {} proof let y be Element of (InclPoset (Ids L)); :: according to LATTICE3:def_8 ::_thesis: ( not y in {} or I <= y ) assume y in {} ; ::_thesis: I <= y hence I <= y ; ::_thesis: verum end; hence ( ex_inf_of {} , InclPoset (Ids L) & "/\" ({},(InclPoset (Ids L))) = [#] L ) by A1, YELLOW_0:31; ::_thesis: verum end; theorem Th48: :: YELLOW_2:48 for L being lower-bounded sup-Semilattice holds InclPoset (Ids L) is complete proof let L be lower-bounded sup-Semilattice; ::_thesis: InclPoset (Ids L) is complete set P = InclPoset (Ids L); for A being Subset of (InclPoset (Ids L)) holds ex_inf_of A, InclPoset (Ids L) proof let A be Subset of (InclPoset (Ids L)); ::_thesis: ex_inf_of A, InclPoset (Ids L) percases ( A = {} or A <> {} ) ; suppose A = {} ; ::_thesis: ex_inf_of A, InclPoset (Ids L) hence ex_inf_of A, InclPoset (Ids L) by Th47; ::_thesis: verum end; suppose A <> {} ; ::_thesis: ex_inf_of A, InclPoset (Ids L) hence ex_inf_of A, InclPoset (Ids L) by Th46; ::_thesis: verum end; end; end; hence InclPoset (Ids L) is complete by Th28; ::_thesis: verum end; registration let L be lower-bounded sup-Semilattice; cluster InclPoset (Ids L) -> complete ; correctness coherence InclPoset (Ids L) is complete ; by Th48; end; begin definition let L be non empty Poset; func SupMap L -> Function of (InclPoset (Ids L)),L means :Def3: :: YELLOW_2:def 3 for I being Ideal of L holds it . I = sup I; existence ex b1 being Function of (InclPoset (Ids L)),L st for I being Ideal of L holds b1 . I = sup I proof deffunc H1( set ) -> Element of the carrier of L = "\/" ($1,L); set P = InclPoset (Ids L); A1: for I being set st I in the carrier of (InclPoset (Ids L)) holds H1(I) in the carrier of L ; ex f being Function of the carrier of (InclPoset (Ids L)), the carrier of L st for I being set st I in the carrier of (InclPoset (Ids L)) holds f . I = H1(I) from FUNCT_2:sch_2(A1); then consider f being Function of the carrier of (InclPoset (Ids L)), the carrier of L such that A2: for I being set st I in the carrier of (InclPoset (Ids L)) holds f . I = "\/" (I,L) ; reconsider f = f as Function of (InclPoset (Ids L)),L ; take f ; ::_thesis: for I being Ideal of L holds f . I = sup I for I being Ideal of L holds f . I = sup I proof let I be Ideal of L; ::_thesis: f . I = sup I I in the carrier of RelStr(# (Ids L),(RelIncl (Ids L)) #) ; then I in the carrier of (InclPoset (Ids L)) by YELLOW_1:def_1; hence f . I = sup I by A2; ::_thesis: verum end; hence for I being Ideal of L holds f . I = sup I ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (InclPoset (Ids L)),L st ( for I being Ideal of L holds b1 . I = sup I ) & ( for I being Ideal of L holds b2 . I = sup I ) holds b1 = b2 proof set P = InclPoset (Ids L); let f, g be Function of (InclPoset (Ids L)),L; ::_thesis: ( ( for I being Ideal of L holds f . I = sup I ) & ( for I being Ideal of L holds g . I = sup I ) implies f = g ) assume that A3: for I being Ideal of L holds f . I = sup I and A4: for I being Ideal of L holds g . I = sup I ; ::_thesis: f = g A5: the carrier of (InclPoset (Ids L)) = the carrier of RelStr(# (Ids L),(RelIncl (Ids L)) #) by YELLOW_1:def_1 .= Ids L ; A6: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(InclPoset_(Ids_L))_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in the carrier of (InclPoset (Ids L)) implies f . x = g . x ) assume x in the carrier of (InclPoset (Ids L)) ; ::_thesis: f . x = g . x then ex I being Ideal of L st x = I by A5; then reconsider I = x as Ideal of L ; f . I = sup I by A3; hence f . x = g . x by A4; ::_thesis: verum end; ( dom f = the carrier of (InclPoset (Ids L)) & dom g = the carrier of (InclPoset (Ids L)) ) by FUNCT_2:def_1; hence f = g by A6, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def3 defines SupMap YELLOW_2:def_3_:_ for L being non empty Poset for b2 being Function of (InclPoset (Ids L)),L holds ( b2 = SupMap L iff for I being Ideal of L holds b2 . I = sup I ); theorem Th49: :: YELLOW_2:49 for L being non empty Poset holds ( dom (SupMap L) = Ids L & rng (SupMap L) is Subset of L ) proof let L be non empty Poset; ::_thesis: ( dom (SupMap L) = Ids L & rng (SupMap L) is Subset of L ) set P = InclPoset (Ids L); thus dom (SupMap L) = the carrier of (InclPoset (Ids L)) by FUNCT_2:def_1 .= the carrier of RelStr(# (Ids L),(RelIncl (Ids L)) #) by YELLOW_1:def_1 .= Ids L ; ::_thesis: rng (SupMap L) is Subset of L thus rng (SupMap L) is Subset of L ; ::_thesis: verum end; theorem :: YELLOW_2:50 for x being set for L being non empty Poset holds ( x in dom (SupMap L) iff x is Ideal of L ) proof let x be set ; ::_thesis: for L being non empty Poset holds ( x in dom (SupMap L) iff x is Ideal of L ) let L be non empty Poset; ::_thesis: ( x in dom (SupMap L) iff x is Ideal of L ) hereby ::_thesis: ( x is Ideal of L implies x in dom (SupMap L) ) assume x in dom (SupMap L) ; ::_thesis: x is Ideal of L then x in Ids L by Th49; then ex I being Ideal of L st x = I ; hence x is Ideal of L ; ::_thesis: verum end; assume x is Ideal of L ; ::_thesis: x in dom (SupMap L) then x in { X where X is Ideal of L : verum } ; hence x in dom (SupMap L) by Th49; ::_thesis: verum end; theorem Th51: :: YELLOW_2:51 for L being non empty up-complete Poset holds SupMap L is monotone proof let L be non empty up-complete Poset; ::_thesis: SupMap L is monotone set P = InclPoset (Ids L); set f = SupMap L; for x, y being Element of (InclPoset (Ids L)) st x <= y holds for a, b being Element of L st a = (SupMap L) . x & b = (SupMap L) . y holds a <= b proof let x, y be Element of (InclPoset (Ids L)); ::_thesis: ( x <= y implies for a, b being Element of L st a = (SupMap L) . x & b = (SupMap L) . y holds a <= b ) assume A1: x <= y ; ::_thesis: for a, b being Element of L st a = (SupMap L) . x & b = (SupMap L) . y holds a <= b reconsider I = x, J = y as Ideal of L by Th41; A2: I c= J by A1, YELLOW_1:3; A3: ( ex_sup_of I,L & ex_sup_of J,L ) by WAYBEL_0:75; A4: ( (SupMap L) . x = sup I & (SupMap L) . y = sup J ) by Def3; let a, b be Element of L; ::_thesis: ( a = (SupMap L) . x & b = (SupMap L) . y implies a <= b ) assume ( a = (SupMap L) . x & b = (SupMap L) . y ) ; ::_thesis: a <= b hence a <= b by A3, A2, A4, YELLOW_0:34; ::_thesis: verum end; hence SupMap L is monotone by ORDERS_3:def_5; ::_thesis: verum end; registration let L be non empty up-complete Poset; cluster SupMap L -> monotone ; correctness coherence SupMap L is monotone ; by Th51; end; definition let L be non empty Poset; func IdsMap L -> Function of L,(InclPoset (Ids L)) means :Def4: :: YELLOW_2:def 4 for x being Element of L holds it . x = downarrow x; existence ex b1 being Function of L,(InclPoset (Ids L)) st for x being Element of L holds b1 . x = downarrow x proof deffunc H1( Element of L) -> Element of bool the carrier of L = downarrow $1; A1: for x being Element of L holds H1(x) is Element of (InclPoset (Ids L)) by Th41; thus ex m being Function of L,(InclPoset (Ids L)) st for x being Element of L holds m . x = H1(x) from FUNCT_2:sch_9(A1); ::_thesis: verum end; uniqueness for b1, b2 being Function of L,(InclPoset (Ids L)) st ( for x being Element of L holds b1 . x = downarrow x ) & ( for x being Element of L holds b2 . x = downarrow x ) holds b1 = b2 proof let f1, f2 be Function of L,(InclPoset (Ids L)); ::_thesis: ( ( for x being Element of L holds f1 . x = downarrow x ) & ( for x being Element of L holds f2 . x = downarrow x ) implies f1 = f2 ) assume that A2: for x being Element of L holds f1 . x = downarrow x and A3: for x being Element of L holds f2 . x = downarrow x ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_Element_of_L_holds_f1_._x_=_f2_._x let x be Element of L; ::_thesis: f1 . x = f2 . x thus f1 . x = downarrow x by A2 .= f2 . x by A3 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines IdsMap YELLOW_2:def_4_:_ for L being non empty Poset for b2 being Function of L,(InclPoset (Ids L)) holds ( b2 = IdsMap L iff for x being Element of L holds b2 . x = downarrow x ); theorem Th52: :: YELLOW_2:52 for L being non empty Poset holds IdsMap L is monotone proof let L be non empty Poset; ::_thesis: IdsMap L is monotone let x1, x2 be Element of L; :: according to ORDERS_3:def_5 ::_thesis: ( not x1 <= x2 or for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds ( not b1 = (IdsMap L) . x1 or not b2 = (IdsMap L) . x2 or b1 <= b2 ) ) assume x1 <= x2 ; ::_thesis: for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds ( not b1 = (IdsMap L) . x1 or not b2 = (IdsMap L) . x2 or b1 <= b2 ) then downarrow x1 c= downarrow x2 by WAYBEL_0:21; then (IdsMap L) . x1 c= downarrow x2 by Def4; then A1: (IdsMap L) . x1 c= (IdsMap L) . x2 by Def4; let a, b be Element of (InclPoset (Ids L)); ::_thesis: ( not a = (IdsMap L) . x1 or not b = (IdsMap L) . x2 or a <= b ) assume ( a = (IdsMap L) . x1 & b = (IdsMap L) . x2 ) ; ::_thesis: a <= b hence a <= b by A1, YELLOW_1:3; ::_thesis: verum end; registration let L be non empty Poset; cluster IdsMap L -> monotone ; correctness coherence IdsMap L is monotone ; by Th52; end; begin definition let L be non empty RelStr ; let F be Relation; func \\/ (F,L) -> Element of L equals :: YELLOW_2:def 5 "\/" ((rng F),L); coherence "\/" ((rng F),L) is Element of L ; func //\ (F,L) -> Element of L equals :: YELLOW_2:def 6 "/\" ((rng F),L); coherence "/\" ((rng F),L) is Element of L ; end; :: deftheorem defines \\/ YELLOW_2:def_5_:_ for L being non empty RelStr for F being Relation holds \\/ (F,L) = "\/" ((rng F),L); :: deftheorem defines //\ YELLOW_2:def_6_:_ for L being non empty RelStr for F being Relation holds //\ (F,L) = "/\" ((rng F),L); notation let J be set ; let L be non empty RelStr ; let F be Function of J, the carrier of L; synonym Sup F for \\/ (L,J); synonym Inf F for //\ (L,J); end; theorem :: YELLOW_2:53 for L being complete LATTICE for J being non empty set for j being Element of J for F being Function of J, the carrier of L holds ( F . j <= Sup & Inf <= F . j ) proof let L be complete LATTICE; ::_thesis: for J being non empty set for j being Element of J for F being Function of J, the carrier of L holds ( F . j <= Sup & Inf <= F . j ) let J be non empty set ; ::_thesis: for j being Element of J for F being Function of J, the carrier of L holds ( F . j <= Sup & Inf <= F . j ) let j be Element of J; ::_thesis: for F being Function of J, the carrier of L holds ( F . j <= Sup & Inf <= F . j ) let F be Function of J, the carrier of L; ::_thesis: ( F . j <= Sup & Inf <= F . j ) F . j in rng F by FUNCT_2:4; hence ( F . j <= Sup & Inf <= F . j ) by Th22; ::_thesis: verum end; theorem :: YELLOW_2:54 for L being complete LATTICE for a being Element of L for J being non empty set for F being Function of J, the carrier of L st ( for j being Element of J holds F . j <= a ) holds Sup <= a proof let L be complete LATTICE; ::_thesis: for a being Element of L for J being non empty set for F being Function of J, the carrier of L st ( for j being Element of J holds F . j <= a ) holds Sup <= a let a be Element of L; ::_thesis: for J being non empty set for F being Function of J, the carrier of L st ( for j being Element of J holds F . j <= a ) holds Sup <= a let J be non empty set ; ::_thesis: for F being Function of J, the carrier of L st ( for j being Element of J holds F . j <= a ) holds Sup <= a let F be Function of J, the carrier of L; ::_thesis: ( ( for j being Element of J holds F . j <= a ) implies Sup <= a ) assume A1: for j being Element of J holds F . j <= a ; ::_thesis: Sup <= a now__::_thesis:_for_c_being_Element_of_L_st_c_in_rng_F_holds_ c_<=_a let c be Element of L; ::_thesis: ( c in rng F implies c <= a ) assume c in rng F ; ::_thesis: c <= a then consider j being set such that A2: j in dom F and A3: c = F . j by FUNCT_1:def_3; reconsider j = j as Element of J by A2; c = F . j by A3; hence c <= a by A1; ::_thesis: verum end; then rng F is_<=_than a by LATTICE3:def_9; hence Sup <= a by YELLOW_0:32; ::_thesis: verum end; theorem :: YELLOW_2:55 for L being complete LATTICE for a being Element of L for J being non empty set for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds a <= Inf proof let L be complete LATTICE; ::_thesis: for a being Element of L for J being non empty set for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds a <= Inf let a be Element of L; ::_thesis: for J being non empty set for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds a <= Inf let J be non empty set ; ::_thesis: for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds a <= Inf let F be Function of J, the carrier of L; ::_thesis: ( ( for j being Element of J holds a <= F . j ) implies a <= Inf ) assume A1: for j being Element of J holds a <= F . j ; ::_thesis: a <= Inf now__::_thesis:_for_c_being_Element_of_L_st_c_in_rng_F_holds_ a_<=_c let c be Element of L; ::_thesis: ( c in rng F implies a <= c ) assume c in rng F ; ::_thesis: a <= c then consider j being set such that A2: j in dom F and A3: c = F . j by FUNCT_1:def_3; reconsider j = j as Element of J by A2; c = F . j by A3; hence a <= c by A1; ::_thesis: verum end; then a is_<=_than rng F by LATTICE3:def_8; hence a <= Inf by YELLOW_0:33; ::_thesis: verum end;