:: LATTICE3 semantic presentation begin deffunc H1( LattStr ) -> set = the carrier of $1; deffunc H2( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_join of $1; deffunc H3( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_meet of $1; definition let X be set ; func BooleLatt X -> strict LattStr means :Def1: :: LATTICE3:def 1 ( the carrier of it = bool X & ( for Y, Z being Subset of X holds ( the L_join of it . (Y,Z) = Y \/ Z & the L_meet of it . (Y,Z) = Y /\ Z ) ) ); existence ex b1 being strict LattStr st ( the carrier of b1 = bool X & ( for Y, Z being Subset of X holds ( the L_join of b1 . (Y,Z) = Y \/ Z & the L_meet of b1 . (Y,Z) = Y /\ Z ) ) ) proof deffunc H4( Subset of X, Subset of X) -> Element of bool X = $1 \/ $2; consider j being BinOp of (bool X) such that A1: for x, y being Subset of X holds j . (x,y) = H4(x,y) from BINOP_1:sch_4(); deffunc H5( Subset of X, Subset of X) -> Element of bool X = $1 /\ $2; consider m being BinOp of (bool X) such that A2: for x, y being Subset of X holds m . (x,y) = H5(x,y) from BINOP_1:sch_4(); take LattStr(# (bool X),j,m #) ; ::_thesis: ( the carrier of LattStr(# (bool X),j,m #) = bool X & ( for Y, Z being Subset of X holds ( the L_join of LattStr(# (bool X),j,m #) . (Y,Z) = Y \/ Z & the L_meet of LattStr(# (bool X),j,m #) . (Y,Z) = Y /\ Z ) ) ) thus ( the carrier of LattStr(# (bool X),j,m #) = bool X & ( for Y, Z being Subset of X holds ( the L_join of LattStr(# (bool X),j,m #) . (Y,Z) = Y \/ Z & the L_meet of LattStr(# (bool X),j,m #) . (Y,Z) = Y /\ Z ) ) ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being strict LattStr st the carrier of b1 = bool X & ( for Y, Z being Subset of X holds ( the L_join of b1 . (Y,Z) = Y \/ Z & the L_meet of b1 . (Y,Z) = Y /\ Z ) ) & the carrier of b2 = bool X & ( for Y, Z being Subset of X holds ( the L_join of b2 . (Y,Z) = Y \/ Z & the L_meet of b2 . (Y,Z) = Y /\ Z ) ) holds b1 = b2 proof let L1, L2 be strict LattStr ; ::_thesis: ( the carrier of L1 = bool X & ( for Y, Z being Subset of X holds ( the L_join of L1 . (Y,Z) = Y \/ Z & the L_meet of L1 . (Y,Z) = Y /\ Z ) ) & the carrier of L2 = bool X & ( for Y, Z being Subset of X holds ( the L_join of L2 . (Y,Z) = Y \/ Z & the L_meet of L2 . (Y,Z) = Y /\ Z ) ) implies L1 = L2 ) assume that A3: the carrier of L1 = bool X and A4: for Y, Z being Subset of X holds ( H2(L1) . (Y,Z) = Y \/ Z & H3(L1) . (Y,Z) = Y /\ Z ) and A5: the carrier of L2 = bool X and A6: for Y, Z being Subset of X holds ( H2(L2) . (Y,Z) = Y \/ Z & H3(L2) . (Y,Z) = Y /\ Z ) ; ::_thesis: L1 = L2 reconsider j1 = H2(L1), j2 = H2(L2), m1 = H3(L1), m2 = H3(L2) as BinOp of (bool X) by A3, A5; now__::_thesis:_for_x,_y_being_Subset_of_X_holds_j1_._(x,y)_=_j2_._(x,y) let x, y be Subset of X; ::_thesis: j1 . (x,y) = j2 . (x,y) thus j1 . (x,y) = x \/ y by A4 .= j2 . (x,y) by A6 ; ::_thesis: verum end; then A7: j1 = j2 by BINOP_1:2; now__::_thesis:_for_x,_y_being_Subset_of_X_holds_m1_._(x,y)_=_m2_._(x,y) let x, y be Subset of X; ::_thesis: m1 . (x,y) = m2 . (x,y) thus m1 . (x,y) = x /\ y by A4 .= m2 . (x,y) by A6 ; ::_thesis: verum end; hence L1 = L2 by A3, A5, A7, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines BooleLatt LATTICE3:def_1_:_ for X being set for b2 being strict LattStr holds ( b2 = BooleLatt X iff ( the carrier of b2 = bool X & ( for Y, Z being Subset of X holds ( the L_join of b2 . (Y,Z) = Y \/ Z & the L_meet of b2 . (Y,Z) = Y /\ Z ) ) ) ); registration let X be set ; cluster BooleLatt X -> non empty strict ; coherence not BooleLatt X is empty proof the carrier of (BooleLatt X) = bool X by Def1; hence not the carrier of (BooleLatt X) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; registration let X be set ; let x, y be Element of (BooleLatt X); let x9, y9 be set ; identifyx "\/" y with x9 \/ y9 when x = x9, y = y9; compatibility ( x = x9 & y = y9 implies x "\/" y = x9 \/ y9 ) proof reconsider x99 = x, y99 = y as Subset of X by Def1; assume that A1: x = x9 and A2: y = y9 ; ::_thesis: x "\/" y = x9 \/ y9 thus x "\/" y = H2( BooleLatt X) . (x99,y99) .= x9 \/ y9 by A1, A2, Def1 ; ::_thesis: verum end; identifyx "/\" y with x9 /\ y9 when x = x9, y = y9; compatibility ( x = x9 & y = y9 implies x "/\" y = x9 /\ y9 ) proof reconsider x99 = x, y99 = y as Subset of X by Def1; assume that A3: x = x9 and A4: y = y9 ; ::_thesis: x "/\" y = x9 /\ y9 thus x "/\" y = H3( BooleLatt X) . (x99,y99) .= x9 /\ y9 by A3, A4, Def1 ; ::_thesis: verum end; end; theorem Th1: :: LATTICE3:1 for X being set for x, y being Element of (BooleLatt X) holds ( x "\/" y = x \/ y & x "/\" y = x /\ y ) ; theorem Th2: :: LATTICE3:2 for X being set for x, y being Element of (BooleLatt X) holds ( x [= y iff x c= y ) proof let X be set ; ::_thesis: for x, y being Element of (BooleLatt X) holds ( x [= y iff x c= y ) let x, y be Element of (BooleLatt X); ::_thesis: ( x [= y iff x c= y ) ( x [= y iff x "\/" y = y ) by LATTICES:def_3; hence ( x [= y iff x c= y ) by XBOOLE_1:7, XBOOLE_1:12; ::_thesis: verum end; registration let X be set ; cluster BooleLatt X -> strict Lattice-like ; coherence BooleLatt X is Lattice-like proof A1: for x, y being Element of (BooleLatt X) holds x "\/" y = y "\/" x ; A2: for x, y, z being Element of (BooleLatt X) holds x "\/" (y "\/" z) = (x "\/" y) "\/" z by XBOOLE_1:4; A3: for x, y being Element of (BooleLatt X) holds (x "/\" y) "\/" y = y by XBOOLE_1:22; A4: for x, y being Element of (BooleLatt X) holds x "/\" y = y "/\" x ; A5: for x, y, z being Element of (BooleLatt X) holds x "/\" (y "/\" z) = (x "/\" y) "/\" z by XBOOLE_1:16; for x, y being Element of (BooleLatt X) holds x "/\" (x "\/" y) = x by XBOOLE_1:21; then ( BooleLatt X is join-commutative & BooleLatt X is join-associative & BooleLatt X is meet-absorbing & BooleLatt X is meet-commutative & BooleLatt X is meet-associative & BooleLatt X is join-absorbing ) by A1, A2, A3, A4, A5, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; hence BooleLatt X is Lattice-like ; ::_thesis: verum end; end; theorem Th3: :: LATTICE3:3 for X being set holds ( BooleLatt X is lower-bounded & Bottom (BooleLatt X) = {} ) proof let X be set ; ::_thesis: ( BooleLatt X is lower-bounded & Bottom (BooleLatt X) = {} ) {} c= X by XBOOLE_1:2; then reconsider x = {} as Element of (BooleLatt X) by Def1; A1: for y being Element of (BooleLatt X) holds x "/\" y = x ; A2: for y being Element of (BooleLatt X) holds y "/\" x = x ; thus BooleLatt X is lower-bounded ::_thesis: Bottom (BooleLatt X) = {} proof take x ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (BooleLatt X) holds ( x "/\" b1 = x & b1 "/\" x = x ) thus for b1 being Element of the carrier of (BooleLatt X) holds ( x "/\" b1 = x & b1 "/\" x = x ) ; ::_thesis: verum end; hence Bottom (BooleLatt X) = {} by A1, A2, LATTICES:def_16; ::_thesis: verum end; theorem Th4: :: LATTICE3:4 for X being set holds ( BooleLatt X is upper-bounded & Top (BooleLatt X) = X ) proof let X be set ; ::_thesis: ( BooleLatt X is upper-bounded & Top (BooleLatt X) = X ) A1: bool X = H1( BooleLatt X) by Def1; then reconsider x = X as Element of (BooleLatt X) by ZFMISC_1:def_1; A2: for y being Element of (BooleLatt X) holds x "\/" y = x by A1, XBOOLE_1:12; A3: for y being Element of (BooleLatt X) holds y "\/" x = x by A1, XBOOLE_1:12; thus BooleLatt X is upper-bounded ::_thesis: Top (BooleLatt X) = X proof take x ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (BooleLatt X) holds ( x "\/" b1 = x & b1 "\/" x = x ) thus for b1 being Element of the carrier of (BooleLatt X) holds ( x "\/" b1 = x & b1 "\/" x = x ) by A1, XBOOLE_1:12; ::_thesis: verum end; hence Top (BooleLatt X) = X by A2, A3, LATTICES:def_17; ::_thesis: verum end; registration let X be set ; cluster BooleLatt X -> strict Boolean ; coherence BooleLatt X is Boolean proof set B = BooleLatt X; A1: BooleLatt X is 0_Lattice by Th3; BooleLatt X is 1_Lattice by Th4; then reconsider B = BooleLatt X as 01_Lattice by A1; A2: B is complemented proof let x be Element of B; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of B st b1 is_a_complement_of x A3: H1(B) = bool X by Def1; reconsider y = X \ x as Element of B by Def1; take y ; ::_thesis: y is_a_complement_of x thus y "\/" x = y \/ x by Th1 .= X \/ x by XBOOLE_1:39 .= X by A3, XBOOLE_1:12 .= Top B by Th4 ; :: according to LATTICES:def_18 ::_thesis: ( x "\/" y = Top B & y "/\" x = Bottom B & x "/\" y = Bottom B ) hence x "\/" y = Top B ; ::_thesis: ( y "/\" x = Bottom B & x "/\" y = Bottom B ) A4: y misses x by XBOOLE_1:79; thus y "/\" x = y /\ x by Th1 .= {} by A4, XBOOLE_0:def_7 .= Bottom B by Th3 ; ::_thesis: x "/\" y = Bottom B hence x "/\" y = Bottom B ; ::_thesis: verum end; B is distributive proof let x, y, z be Element of B; :: according to LATTICES:def_11 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) thus x "/\" (y "\/" z) = x /\ (y "\/" z) by Th1 .= x /\ (y \/ z) by Th1 .= (x /\ y) \/ (x /\ z) by XBOOLE_1:23 .= (x "/\" y) \/ (x /\ z) by Th1 .= (x "/\" y) \/ (x "/\" z) by Th1 .= (x "/\" y) "\/" (x "/\" z) by Th1 ; ::_thesis: verum end; hence BooleLatt X is Boolean by A2; ::_thesis: verum end; end; theorem :: LATTICE3:5 for X being set for x being Element of (BooleLatt X) holds x ` = X \ x proof let X be set ; ::_thesis: for x being Element of (BooleLatt X) holds x ` = X \ x set B = BooleLatt X; let x be Element of (BooleLatt X); ::_thesis: x ` = X \ x A1: (x `) "/\" x = Bottom (BooleLatt X) by LATTICES:20; A2: x "\/" (x `) = Top (BooleLatt X) by LATTICES:21; A3: Bottom (BooleLatt X) = {} by Th3; A4: Top (BooleLatt X) = X by Th4; A5: x ` misses x by A1, A3, XBOOLE_0:def_7; A6: X \ x = (x \ x) \/ ((x `) \ x) by A2, A4, XBOOLE_1:42; x \ x = {} by XBOOLE_1:37; hence x ` = X \ x by A5, A6, XBOOLE_1:83; ::_thesis: verum end; begin definition let L be Lattice; :: original: LattRel redefine func LattRel L -> Order of the carrier of L; coherence LattRel L is Order of the carrier of L proof A1: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def_8; LattRel L c= [:H1(L),H1(L):] proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in LattRel L or [x,y] in [:H1(L),H1(L):] ) assume [x,y] in LattRel L ; ::_thesis: [x,y] in [:H1(L),H1(L):] then ex p, q being Element of L st ( [x,y] = [p,q] & p [= q ) by A1; hence [x,y] in [:H1(L),H1(L):] by ZFMISC_1:87; ::_thesis: verum end; then reconsider R = LattRel L as Relation of H1(L) ; A2: R is_reflexive_in H1(L) proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in H1(L) or [x,x] in R ) assume x in H1(L) ; ::_thesis: [x,x] in R then reconsider x = x as Element of L ; x [= x ; hence [x,x] in R by FILTER_1:31; ::_thesis: verum end; A3: R is_antisymmetric_in H1(L) proof let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in H1(L) or not y in H1(L) or not [x,y] in R or not [y,x] in R or x = y ) assume that A4: x in H1(L) and A5: y in H1(L) ; ::_thesis: ( not [x,y] in R or not [y,x] in R or x = y ) reconsider x9 = x, y9 = y as Element of L by A4, A5; assume that A6: [x,y] in R and A7: [y,x] in R ; ::_thesis: x = y A8: x9 [= y9 by A6, FILTER_1:31; y9 [= x9 by A7, FILTER_1:31; hence x = y by A8, LATTICES:8; ::_thesis: verum end; A9: R is_transitive_in H1(L) proof let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in H1(L) or not y in H1(L) or not z in H1(L) or not [x,y] in R or not [y,z] in R or [x,z] in R ) assume that A10: x in H1(L) and A11: y in H1(L) and A12: z in H1(L) ; ::_thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R ) reconsider x9 = x, y9 = y, z9 = z as Element of L by A10, A11, A12; assume that A13: [x,y] in R and A14: [y,z] in R ; ::_thesis: [x,z] in R A15: x9 [= y9 by A13, FILTER_1:31; y9 [= z9 by A14, FILTER_1:31; then x9 [= z9 by A15, LATTICES:7; hence [x,z] in R by FILTER_1:31; ::_thesis: verum end; A16: dom R = H1(L) by A2, ORDERS_1:13; field R = H1(L) by A2, ORDERS_1:13; hence LattRel L is Order of the carrier of L by A2, A3, A9, A16, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_16; ::_thesis: verum end; end; definition let L be Lattice; func LattPOSet L -> strict Poset equals :: LATTICE3:def 2 RelStr(# the carrier of L,(LattRel L) #); correctness coherence RelStr(# the carrier of L,(LattRel L) #) is strict Poset; ; end; :: deftheorem defines LattPOSet LATTICE3:def_2_:_ for L being Lattice holds LattPOSet L = RelStr(# the carrier of L,(LattRel L) #); registration let L be Lattice; cluster LattPOSet L -> non empty strict ; coherence not LattPOSet L is empty ; end; theorem Th6: :: LATTICE3:6 for L1, L2 being Lattice st LattPOSet L1 = LattPOSet L2 holds LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) proof let L1, L2 be Lattice; ::_thesis: ( LattPOSet L1 = LattPOSet L2 implies LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ) assume A1: LattPOSet L1 = LattPOSet L2 ; ::_thesis: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) reconsider j = H2(L2), m = H3(L2) as BinOp of H1(L1) by A1; now__::_thesis:_for_a,_b_being_Element_of_L1_holds_H2(L1)_._(a,b)_=_j_._(a,b) let a, b be Element of L1; ::_thesis: H2(L1) . (a,b) = j . (a,b) reconsider x = a, y = b, xy = a "\/" b as Element of L2 by A1; reconsider ab = x "\/" y as Element of L1 by A1; A2: a [= a "\/" b by LATTICES:5; A3: b [= b "\/" a by LATTICES:5; A4: x [= x "\/" y by LATTICES:5; A5: y [= y "\/" x by LATTICES:5; A6: [x,xy] in LattRel L2 by A1, A2, FILTER_1:31; A7: [y,xy] in LattRel L2 by A1, A3, FILTER_1:31; A8: [a,ab] in LattRel L1 by A1, A4, FILTER_1:31; A9: [b,ab] in LattRel L1 by A1, A5, FILTER_1:31; A10: a [= ab by A8, FILTER_1:31; A11: b [= ab by A9, FILTER_1:31; A12: x [= xy by A6, FILTER_1:31; A13: y [= xy by A7, FILTER_1:31; A14: a "\/" b [= ab by A10, A11, FILTER_0:6; x "\/" y [= xy by A12, A13, FILTER_0:6; then [ab,(a "\/" b)] in LattRel L1 by A1, FILTER_1:31; then ab [= a "\/" b by FILTER_1:31; hence H2(L1) . (a,b) = j . (a,b) by A14, LATTICES:8; ::_thesis: verum end; then A15: H2(L1) = j by BINOP_1:2; now__::_thesis:_for_a,_b_being_Element_of_L1_holds_H3(L1)_._(a,b)_=_m_._(a,b) let a, b be Element of L1; ::_thesis: H3(L1) . (a,b) = m . (a,b) reconsider x = a, y = b, xy = a "/\" b as Element of L2 by A1; reconsider ab = x "/\" y as Element of L1 by A1; A16: a "/\" b [= a by LATTICES:6; A17: b "/\" a [= b by LATTICES:6; A18: x "/\" y [= x by LATTICES:6; A19: y "/\" x [= y by LATTICES:6; A20: [xy,x] in LattRel L2 by A1, A16, FILTER_1:31; A21: [xy,y] in LattRel L2 by A1, A17, FILTER_1:31; A22: [ab,a] in LattRel L1 by A1, A18, FILTER_1:31; A23: [ab,b] in LattRel L1 by A1, A19, FILTER_1:31; A24: ab [= a by A22, FILTER_1:31; A25: ab [= b by A23, FILTER_1:31; A26: xy [= x by A20, FILTER_1:31; A27: xy [= y by A21, FILTER_1:31; A28: ab [= a "/\" b by A24, A25, FILTER_0:7; xy [= x "/\" y by A26, A27, FILTER_0:7; then [(a "/\" b),ab] in LattRel L1 by A1, FILTER_1:31; then a "/\" b [= ab by FILTER_1:31; hence H3(L1) . (a,b) = m . (a,b) by A28, LATTICES:8; ::_thesis: verum end; hence LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) by A1, A15, BINOP_1:2; ::_thesis: verum end; definition let L be Lattice; let p be Element of L; funcp % -> Element of (LattPOSet L) equals :: LATTICE3:def 3 p; correctness coherence p is Element of (LattPOSet L); ; end; :: deftheorem defines % LATTICE3:def_3_:_ for L being Lattice for p being Element of L holds p % = p; definition let L be Lattice; let p be Element of (LattPOSet L); func % p -> Element of L equals :: LATTICE3:def 4 p; correctness coherence p is Element of L; ; end; :: deftheorem defines % LATTICE3:def_4_:_ for L being Lattice for p being Element of (LattPOSet L) holds % p = p; theorem Th7: :: LATTICE3:7 for L being Lattice for p, q being Element of L holds ( p [= q iff p % <= q % ) proof let L be Lattice; ::_thesis: for p, q being Element of L holds ( p [= q iff p % <= q % ) let p, q be Element of L; ::_thesis: ( p [= q iff p % <= q % ) ( p [= q iff [p,q] in LattRel L ) by FILTER_1:31; hence ( p [= q iff p % <= q % ) by ORDERS_2:def_5; ::_thesis: verum end; definition let X be set ; let O be Order of X; :: original: ~ redefine funcO ~ -> Order of X; coherence O ~ is Order of X proof A1: dom O = dom (O ~) by RELAT_2:12; dom O = X by PARTFUN1:def_2; hence O ~ is Order of X by A1, PARTFUN1:def_2; ::_thesis: verum end; end; definition let A be RelStr ; funcA ~ -> strict RelStr equals :: LATTICE3:def 5 RelStr(# the carrier of A,( the InternalRel of A ~) #); correctness coherence RelStr(# the carrier of A,( the InternalRel of A ~) #) is strict RelStr ; ; end; :: deftheorem defines ~ LATTICE3:def_5_:_ for A being RelStr holds A ~ = RelStr(# the carrier of A,( the InternalRel of A ~) #); registration let A be Poset; clusterA ~ -> strict reflexive transitive antisymmetric ; coherence ( A ~ is reflexive & A ~ is transitive & A ~ is antisymmetric ) proof A ~ = RelStr(# the carrier of A,( the InternalRel of A ~) #) ; hence ( A ~ is reflexive & A ~ is transitive & A ~ is antisymmetric ) ; ::_thesis: verum end; end; registration let A be non empty RelStr ; clusterA ~ -> non empty strict ; coherence not A ~ is empty ; end; theorem :: LATTICE3:8 for A being RelStr holds (A ~) ~ = RelStr(# the carrier of A, the InternalRel of A #) ; definition let A be RelStr ; let a be Element of A; funca ~ -> Element of (A ~) equals :: LATTICE3:def 6 a; correctness coherence a is Element of (A ~); ; end; :: deftheorem defines ~ LATTICE3:def_6_:_ for A being RelStr for a being Element of A holds a ~ = a; definition let A be RelStr ; let a be Element of (A ~); func ~ a -> Element of A equals :: LATTICE3:def 7 a; correctness coherence a is Element of A; ; end; :: deftheorem defines ~ LATTICE3:def_7_:_ for A being RelStr for a being Element of (A ~) holds ~ a = a; theorem Th9: :: LATTICE3:9 for A being RelStr for a, b being Element of A holds ( a <= b iff b ~ <= a ~ ) proof let A be RelStr ; ::_thesis: for a, b being Element of A holds ( a <= b iff b ~ <= a ~ ) let a, b be Element of A; ::_thesis: ( a <= b iff b ~ <= a ~ ) A1: ( a <= b iff [a,b] in the InternalRel of A ) by ORDERS_2:def_5; ( b ~ <= a ~ iff [(b ~),(a ~)] in the InternalRel of (A ~) ) by ORDERS_2:def_5; hence ( a <= b iff b ~ <= a ~ ) by A1, RELAT_1:def_7; ::_thesis: verum end; definition let A be RelStr ; let X be set ; let a be Element of A; preda is_<=_than X means :: LATTICE3:def 8 for b being Element of A st b in X holds a <= b; predX is_<=_than a means :Def9: :: LATTICE3:def 9 for b being Element of A st b in X holds b <= a; end; :: deftheorem defines is_<=_than LATTICE3:def_8_:_ for A being RelStr for X being set for a being Element of A holds ( a is_<=_than X iff for b being Element of A st b in X holds a <= b ); :: deftheorem Def9 defines is_<=_than LATTICE3:def_9_:_ for A being RelStr for X being set for a being Element of A holds ( X is_<=_than a iff for b being Element of A st b in X holds b <= a ); notation let A be RelStr ; let X be set ; let a be Element of A; synonym X is_>=_than a for a is_<=_than X; synonym a is_>=_than X for X is_<=_than a; end; definition let IT be RelStr ; attrIT is with_suprema means :Def10: :: LATTICE3:def 10 for x, y being Element of IT ex z being Element of IT st ( x <= z & y <= z & ( for z9 being Element of IT st x <= z9 & y <= z9 holds z <= z9 ) ); attrIT is with_infima means :Def11: :: LATTICE3:def 11 for x, y being Element of IT ex z being Element of IT st ( z <= x & z <= y & ( for z9 being Element of IT st z9 <= x & z9 <= y holds z9 <= z ) ); end; :: deftheorem Def10 defines with_suprema LATTICE3:def_10_:_ for IT being RelStr holds ( IT is with_suprema iff for x, y being Element of IT ex z being Element of IT st ( x <= z & y <= z & ( for z9 being Element of IT st x <= z9 & y <= z9 holds z <= z9 ) ) ); :: deftheorem Def11 defines with_infima LATTICE3:def_11_:_ for IT being RelStr holds ( IT is with_infima iff for x, y being Element of IT ex z being Element of IT st ( z <= x & z <= y & ( for z9 being Element of IT st z9 <= x & z9 <= y holds z9 <= z ) ) ); registration cluster with_suprema -> non empty for RelStr ; coherence for b1 being RelStr st b1 is with_suprema holds not b1 is empty proof let A be RelStr ; ::_thesis: ( A is with_suprema implies not A is empty ) assume A1: for x, y being Element of A ex z being Element of A st ( x <= z & y <= z & ( for z9 being Element of A st x <= z9 & y <= z9 holds z <= z9 ) ) ; :: according to LATTICE3:def_10 ::_thesis: not A is empty set x = the Element of A; consider z being Element of A such that A2: the Element of A <= z and the Element of A <= z and for z9 being Element of A st the Element of A <= z9 & the Element of A <= z9 holds z <= z9 by A1; [ the Element of A,z] in the InternalRel of A by A2, ORDERS_2:def_5; hence not A is empty ; ::_thesis: verum end; cluster with_infima -> non empty for RelStr ; coherence for b1 being RelStr st b1 is with_infima holds not b1 is empty proof let A be RelStr ; ::_thesis: ( A is with_infima implies not A is empty ) assume A3: for x, y being Element of A ex z being Element of A st ( x >= z & y >= z & ( for z9 being Element of A st x >= z9 & y >= z9 holds z >= z9 ) ) ; :: according to LATTICE3:def_11 ::_thesis: not A is empty set x = the Element of A; consider z being Element of A such that A4: the Element of A >= z and the Element of A >= z and for z9 being Element of A st the Element of A >= z9 & the Element of A >= z9 holds z >= z9 by A3; [z, the Element of A] in the InternalRel of A by A4, ORDERS_2:def_5; hence not A is empty ; ::_thesis: verum end; end; theorem :: LATTICE3:10 for A being RelStr holds ( A is with_suprema iff A ~ is with_infima ) proof let A be RelStr ; ::_thesis: ( A is with_suprema iff A ~ is with_infima ) thus ( A is with_suprema implies A ~ is with_infima ) ::_thesis: ( A ~ is with_infima implies A is with_suprema ) proof assume A1: for a, b being Element of A ex c being Element of A st ( a <= c & b <= c & ( for c9 being Element of A st a <= c9 & b <= c9 holds c <= c9 ) ) ; :: according to LATTICE3:def_10 ::_thesis: A ~ is with_infima let x, y be Element of (A ~); :: according to LATTICE3:def_11 ::_thesis: ex z being Element of (A ~) st ( z <= x & z <= y & ( for z9 being Element of (A ~) st z9 <= x & z9 <= y holds z9 <= z ) ) consider c being Element of A such that A2: ~ x <= c and A3: ~ y <= c and A4: for c9 being Element of A st ~ x <= c9 & ~ y <= c9 holds c <= c9 by A1; take z = c ~ ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of (A ~) st z9 <= x & z9 <= y holds z9 <= z ) ) A5: (~ x) ~ = ~ x ; A6: (~ y) ~ = ~ y ; hence ( z <= x & z <= y ) by A2, A3, A5, Th9; ::_thesis: for z9 being Element of (A ~) st z9 <= x & z9 <= y holds z9 <= z let z9 be Element of (A ~); ::_thesis: ( z9 <= x & z9 <= y implies z9 <= z ) A7: (~ z9) ~ = ~ z9 ; assume that A8: z9 <= x and A9: z9 <= y ; ::_thesis: z9 <= z A10: ~ x <= ~ z9 by A5, A7, A8, Th9; ~ y <= ~ z9 by A6, A7, A9, Th9; then c <= ~ z9 by A4, A10; hence z9 <= z by A7, Th9; ::_thesis: verum end; assume A11: for x, y being Element of (A ~) ex z being Element of (A ~) st ( z <= x & z <= y & ( for z9 being Element of (A ~) st z9 <= x & z9 <= y holds z9 <= z ) ) ; :: according to LATTICE3:def_11 ::_thesis: A is with_suprema let a be Element of A; :: according to LATTICE3:def_10 ::_thesis: for y being Element of A ex z being Element of A st ( a <= z & y <= z & ( for z9 being Element of A st a <= z9 & y <= z9 holds z <= z9 ) ) let b be Element of A; ::_thesis: ex z being Element of A st ( a <= z & b <= z & ( for z9 being Element of A st a <= z9 & b <= z9 holds z <= z9 ) ) consider z being Element of (A ~) such that A12: z <= a ~ and A13: z <= b ~ and A14: for z9 being Element of (A ~) st z9 <= a ~ & z9 <= b ~ holds z9 <= z by A11; take c = ~ z; ::_thesis: ( a <= c & b <= c & ( for z9 being Element of A st a <= z9 & b <= z9 holds c <= z9 ) ) A15: (~ z) ~ = ~ z ; hence ( a <= c & b <= c ) by A12, A13, Th9; ::_thesis: for z9 being Element of A st a <= z9 & b <= z9 holds c <= z9 let c9 be Element of A; ::_thesis: ( a <= c9 & b <= c9 implies c <= c9 ) assume that A16: a <= c9 and A17: b <= c9 ; ::_thesis: c <= c9 A18: c9 ~ <= a ~ by A16, Th9; c9 ~ <= b ~ by A17, Th9; then c9 ~ <= z by A14, A18; hence c <= c9 by A15, Th9; ::_thesis: verum end; theorem :: LATTICE3:11 for L being Lattice holds ( LattPOSet L is with_suprema & LattPOSet L is with_infima ) proof let L be Lattice; ::_thesis: ( LattPOSet L is with_suprema & LattPOSet L is with_infima ) thus LattPOSet L is with_suprema ::_thesis: LattPOSet L is with_infima proof let x, y be Element of (LattPOSet L); :: according to LATTICE3:def_10 ::_thesis: ex z being Element of (LattPOSet L) st ( x <= z & y <= z & ( for z9 being Element of (LattPOSet L) st x <= z9 & y <= z9 holds z <= z9 ) ) take z = ((% x) "\/" (% y)) % ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of (LattPOSet L) st x <= z9 & y <= z9 holds z <= z9 ) ) A1: % x [= (% x) "\/" (% y) by LATTICES:5; A2: % y [= (% y) "\/" (% x) by LATTICES:5; A3: (% x) % = % x ; A4: (% y) % = % y ; hence ( x <= z & y <= z ) by A1, A2, A3, Th7; ::_thesis: for z9 being Element of (LattPOSet L) st x <= z9 & y <= z9 holds z <= z9 let z9 be Element of (LattPOSet L); ::_thesis: ( x <= z9 & y <= z9 implies z <= z9 ) A5: (% z9) % = % z9 ; assume that A6: x <= z9 and A7: y <= z9 ; ::_thesis: z <= z9 A8: % x [= % z9 by A3, A5, A6, Th7; % y [= % z9 by A4, A5, A7, Th7; then (% x) "\/" (% y) [= % z9 by A8, FILTER_0:6; hence z <= z9 by A5, Th7; ::_thesis: verum end; let x, y be Element of (LattPOSet L); :: according to LATTICE3:def_11 ::_thesis: ex z being Element of (LattPOSet L) st ( z <= x & z <= y & ( for z9 being Element of (LattPOSet L) st z9 <= x & z9 <= y holds z9 <= z ) ) take z = ((% x) "/\" (% y)) % ; ::_thesis: ( z <= x & z <= y & ( for z9 being Element of (LattPOSet L) st z9 <= x & z9 <= y holds z9 <= z ) ) A9: (% x) "/\" (% y) [= % x by LATTICES:6; A10: (% y) "/\" (% x) [= % y by LATTICES:6; A11: (% x) % = % x ; A12: (% y) % = % y ; hence ( z <= x & z <= y ) by A9, A10, A11, Th7; ::_thesis: for z9 being Element of (LattPOSet L) st z9 <= x & z9 <= y holds z9 <= z let z9 be Element of (LattPOSet L); ::_thesis: ( z9 <= x & z9 <= y implies z9 <= z ) A13: (% z9) % = % z9 ; assume that A14: z9 <= x and A15: z9 <= y ; ::_thesis: z9 <= z A16: % z9 [= % x by A11, A13, A14, Th7; % z9 [= % y by A12, A13, A15, Th7; then % z9 [= (% x) "/\" (% y) by A16, FILTER_0:7; hence z9 <= z by A13, Th7; ::_thesis: verum end; definition let IT be RelStr ; attrIT is complete means :Def12: :: LATTICE3:def 12 for X being set ex a being Element of IT st ( X is_<=_than a & ( for b being Element of IT st X is_<=_than b holds a <= b ) ); end; :: deftheorem Def12 defines complete LATTICE3:def_12_:_ for IT being RelStr holds ( IT is complete iff for X being set ex a being Element of IT st ( X is_<=_than a & ( for b being Element of IT st X is_<=_than b holds a <= b ) ) ); registration cluster non empty strict V58() reflexive transitive antisymmetric complete for RelStr ; existence ex b1 being Poset st ( b1 is strict & b1 is complete & not b1 is empty ) proof set s = the set ; set D = { the set }; set R = the Order of { the set }; take A = RelStr(# { the set }, the Order of { the set } #); ::_thesis: ( A is strict & A is complete & not A is empty ) thus A is strict ; ::_thesis: ( A is complete & not A is empty ) hereby :: according to LATTICE3:def_12 ::_thesis: not A is empty let X be set ; ::_thesis: ex s being Element of A st ( X is_<=_than s & ( for b being Element of A st X is_<=_than b holds s <= b ) ) reconsider s = the set as Element of A by TARSKI:def_1; take s = s; ::_thesis: ( X is_<=_than s & ( for b being Element of A st X is_<=_than b holds s <= b ) ) thus X is_<=_than s ::_thesis: for b being Element of A st X is_<=_than b holds s <= b proof let a be Element of A; :: according to LATTICE3:def_9 ::_thesis: ( a in X implies a <= s ) assume a in X ; ::_thesis: a <= s thus a <= s by TARSKI:def_1; ::_thesis: verum end; let b be Element of A; ::_thesis: ( X is_<=_than b implies s <= b ) assume X is_<=_than b ; ::_thesis: s <= b thus s <= b by TARSKI:def_1; ::_thesis: verum end; thus not A is empty ; ::_thesis: verum end; end; theorem Th12: :: LATTICE3:12 for A being non empty RelStr st A is complete holds ( A is with_suprema & A is with_infima ) proof let A be non empty RelStr ; ::_thesis: ( A is complete implies ( A is with_suprema & A is with_infima ) ) assume A1: for X being set ex a being Element of A st ( X is_<=_than a & ( for b being Element of A st X is_<=_than b holds a <= b ) ) ; :: according to LATTICE3:def_12 ::_thesis: ( A is with_suprema & A is with_infima ) thus A is with_suprema ::_thesis: A is with_infima proof let a be Element of A; :: according to LATTICE3:def_10 ::_thesis: for y being Element of A ex z being Element of A st ( a <= z & y <= z & ( for z9 being Element of A st a <= z9 & y <= z9 holds z <= z9 ) ) let b be Element of A; ::_thesis: ex z being Element of A st ( a <= z & b <= z & ( for z9 being Element of A st a <= z9 & b <= z9 holds z <= z9 ) ) consider c being Element of A such that A2: {a,b} is_<=_than c and A3: for c9 being Element of A st {a,b} is_<=_than c9 holds c <= c9 by A1; take c ; ::_thesis: ( a <= c & b <= c & ( for z9 being Element of A st a <= z9 & b <= z9 holds c <= z9 ) ) A4: a in {a,b} by TARSKI:def_2; b in {a,b} by TARSKI:def_2; hence ( a <= c & b <= c ) by A2, A4, Def9; ::_thesis: for z9 being Element of A st a <= z9 & b <= z9 holds c <= z9 let c9 be Element of A; ::_thesis: ( a <= c9 & b <= c9 implies c <= c9 ) assume that A5: a <= c9 and A6: b <= c9 ; ::_thesis: c <= c9 {a,b} is_<=_than c9 proof let d be Element of A; :: according to LATTICE3:def_9 ::_thesis: ( d in {a,b} implies d <= c9 ) assume d in {a,b} ; ::_thesis: d <= c9 hence d <= c9 by A5, A6, TARSKI:def_2; ::_thesis: verum end; hence c <= c9 by A3; ::_thesis: verum end; let a be Element of A; :: according to LATTICE3:def_11 ::_thesis: for y being Element of A ex z being Element of A st ( z <= a & z <= y & ( for z9 being Element of A st z9 <= a & z9 <= y holds z9 <= z ) ) let b be Element of A; ::_thesis: ex z being Element of A st ( z <= a & z <= b & ( for z9 being Element of A st z9 <= a & z9 <= b holds z9 <= z ) ) set X = { c where c is Element of A : ( c <= a & c <= b ) } ; consider c being Element of A such that A7: { c where c is Element of A : ( c <= a & c <= b ) } is_<=_than c and A8: for c9 being Element of A st { c where c is Element of A : ( c <= a & c <= b ) } is_<=_than c9 holds c <= c9 by A1; take c ; ::_thesis: ( c <= a & c <= b & ( for z9 being Element of A st z9 <= a & z9 <= b holds z9 <= c ) ) { c where c is Element of A : ( c <= a & c <= b ) } is_<=_than a proof let c be Element of A; :: according to LATTICE3:def_9 ::_thesis: ( c in { c where c is Element of A : ( c <= a & c <= b ) } implies c <= a ) assume c in { c where c is Element of A : ( c <= a & c <= b ) } ; ::_thesis: c <= a then ex c9 being Element of A st ( c = c9 & c9 <= a & c9 <= b ) ; hence c <= a ; ::_thesis: verum end; hence c <= a by A8; ::_thesis: ( c <= b & ( for z9 being Element of A st z9 <= a & z9 <= b holds z9 <= c ) ) { c where c is Element of A : ( c <= a & c <= b ) } is_<=_than b proof let c be Element of A; :: according to LATTICE3:def_9 ::_thesis: ( c in { c where c is Element of A : ( c <= a & c <= b ) } implies c <= b ) assume c in { c where c is Element of A : ( c <= a & c <= b ) } ; ::_thesis: c <= b then ex c9 being Element of A st ( c = c9 & c9 <= a & c9 <= b ) ; hence c <= b ; ::_thesis: verum end; hence c <= b by A8; ::_thesis: for z9 being Element of A st z9 <= a & z9 <= b holds z9 <= c let c9 be Element of A; ::_thesis: ( c9 <= a & c9 <= b implies c9 <= c ) assume that A9: c9 <= a and A10: c9 <= b ; ::_thesis: c9 <= c c9 in { c where c is Element of A : ( c <= a & c <= b ) } by A9, A10; hence c9 <= c by A7, Def9; ::_thesis: verum end; registration cluster non empty strict V58() reflexive transitive antisymmetric with_suprema with_infima complete for RelStr ; existence ex b1 being Poset st ( b1 is complete & b1 is with_suprema & b1 is with_infima & b1 is strict & not b1 is empty ) proof set A = the non empty strict complete Poset; take the non empty strict complete Poset ; ::_thesis: ( the non empty strict complete Poset is complete & the non empty strict complete Poset is with_suprema & the non empty strict complete Poset is with_infima & the non empty strict complete Poset is strict & not the non empty strict complete Poset is empty ) thus ( the non empty strict complete Poset is complete & the non empty strict complete Poset is with_suprema & the non empty strict complete Poset is with_infima & the non empty strict complete Poset is strict & not the non empty strict complete Poset is empty ) by Th12; ::_thesis: verum end; end; definition let A be RelStr ; assume B1: A is antisymmetric ; let a, b be Element of A; assume B2: ex x being Element of A st ( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds x <= c ) ) ; funca "\/" b -> Element of A means :Def13: :: LATTICE3:def 13 ( a <= it & b <= it & ( for c being Element of A st a <= c & b <= c holds it <= c ) ); existence ex b1 being Element of A st ( a <= b1 & b <= b1 & ( for c being Element of A st a <= c & b <= c holds b1 <= c ) ) by B2; uniqueness for b1, b2 being Element of A st a <= b1 & b <= b1 & ( for c being Element of A st a <= c & b <= c holds b1 <= c ) & a <= b2 & b <= b2 & ( for c being Element of A st a <= c & b <= c holds b2 <= c ) holds b1 = b2 proof let c1, c2 be Element of A; ::_thesis: ( a <= c1 & b <= c1 & ( for c being Element of A st a <= c & b <= c holds c1 <= c ) & a <= c2 & b <= c2 & ( for c being Element of A st a <= c & b <= c holds c2 <= c ) implies c1 = c2 ) assume that A1: a <= c1 and A2: b <= c1 and A3: for c being Element of A st a <= c & b <= c holds c1 <= c and A4: a <= c2 and A5: b <= c2 and A6: for c being Element of A st a <= c & b <= c holds c2 <= c ; ::_thesis: c1 = c2 A7: c1 <= c2 by A3, A4, A5; c2 <= c1 by A1, A2, A6; hence c1 = c2 by B1, A7, ORDERS_2:2; ::_thesis: verum end; end; :: deftheorem Def13 defines "\/" LATTICE3:def_13_:_ for A being RelStr st A is antisymmetric holds for a, b being Element of A st ex x being Element of A st ( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds x <= c ) ) holds for b4 being Element of A holds ( b4 = a "\/" b iff ( a <= b4 & b <= b4 & ( for c being Element of A st a <= c & b <= c holds b4 <= c ) ) ); Lm1: now__::_thesis:_for_A_being_non_empty_antisymmetric_with_suprema_RelStr_ for_a,_b,_c_being_Element_of_A_holds_ (_c_=_a_"\/"_b_iff_(_a_<=_c_&_b_<=_c_&_(_for_d_being_Element_of_A_st_a_<=_d_&_b_<=_d_holds_ c_<=_d_)_)_) let A be non empty antisymmetric with_suprema RelStr ; ::_thesis: for a, b, c being Element of A holds ( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds c <= d ) ) ) let a, b be Element of A; ::_thesis: for c being Element of A holds ( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds c <= d ) ) ) ex x being Element of A st ( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds x <= c ) ) by Def10; hence for c being Element of A holds ( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds c <= d ) ) ) by Def13; ::_thesis: verum end; definition let A be RelStr ; assume B1: A is antisymmetric ; let a, b be Element of A; assume B2: ex x being Element of A st ( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds x >= c ) ) ; funca "/\" b -> Element of A means :Def14: :: LATTICE3:def 14 ( it <= a & it <= b & ( for c being Element of A st c <= a & c <= b holds c <= it ) ); existence ex b1 being Element of A st ( b1 <= a & b1 <= b & ( for c being Element of A st c <= a & c <= b holds c <= b1 ) ) by B2; uniqueness for b1, b2 being Element of A st b1 <= a & b1 <= b & ( for c being Element of A st c <= a & c <= b holds c <= b1 ) & b2 <= a & b2 <= b & ( for c being Element of A st c <= a & c <= b holds c <= b2 ) holds b1 = b2 proof let c1, c2 be Element of A; ::_thesis: ( c1 <= a & c1 <= b & ( for c being Element of A st c <= a & c <= b holds c <= c1 ) & c2 <= a & c2 <= b & ( for c being Element of A st c <= a & c <= b holds c <= c2 ) implies c1 = c2 ) assume that A1: c1 <= a and A2: c1 <= b and A3: for c being Element of A st c <= a & c <= b holds c <= c1 and A4: c2 <= a and A5: c2 <= b and A6: for c being Element of A st c <= a & c <= b holds c <= c2 ; ::_thesis: c1 = c2 A7: c1 <= c2 by A1, A2, A6; c2 <= c1 by A3, A4, A5; hence c1 = c2 by B1, A7, ORDERS_2:2; ::_thesis: verum end; end; :: deftheorem Def14 defines "/\" LATTICE3:def_14_:_ for A being RelStr st A is antisymmetric holds for a, b being Element of A st ex x being Element of A st ( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds x >= c ) ) holds for b4 being Element of A holds ( b4 = a "/\" b iff ( b4 <= a & b4 <= b & ( for c being Element of A st c <= a & c <= b holds c <= b4 ) ) ); Lm2: now__::_thesis:_for_A_being_non_empty_antisymmetric_with_infima_RelStr_ for_a,_b,_c_being_Element_of_A_holds_ (_c_=_a_"/\"_b_iff_(_a_>=_c_&_b_>=_c_&_(_for_d_being_Element_of_A_st_a_>=_d_&_b_>=_d_holds_ c_>=_d_)_)_) let A be non empty antisymmetric with_infima RelStr ; ::_thesis: for a, b, c being Element of A holds ( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds c >= d ) ) ) let a, b be Element of A; ::_thesis: for c being Element of A holds ( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds c >= d ) ) ) ex x being Element of A st ( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds x >= c ) ) by Def11; hence for c being Element of A holds ( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds c >= d ) ) ) by Def14; ::_thesis: verum end; theorem Th13: :: LATTICE3:13 for V being antisymmetric with_suprema RelStr for u1, u2 being Element of V holds u1 "\/" u2 = u2 "\/" u1 proof let V be antisymmetric with_suprema RelStr ; ::_thesis: for u1, u2 being Element of V holds u1 "\/" u2 = u2 "\/" u1 let u1, u2 be Element of V; ::_thesis: u1 "\/" u2 = u2 "\/" u1 A1: u1 <= u1 "\/" u2 by Lm1; A2: u2 <= u1 "\/" u2 by Lm1; for u3 being Element of V st u2 <= u3 & u1 <= u3 holds u1 "\/" u2 <= u3 by Lm1; hence u1 "\/" u2 = u2 "\/" u1 by A1, A2, Def13; ::_thesis: verum end; theorem Th14: :: LATTICE3:14 for V being antisymmetric with_suprema RelStr for u1, u2, u3 being Element of V st V is transitive holds (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) proof let V be antisymmetric with_suprema RelStr ; ::_thesis: for u1, u2, u3 being Element of V st V is transitive holds (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) let u1, u2, u3 be Element of V; ::_thesis: ( V is transitive implies (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) ) assume A1: V is transitive ; ::_thesis: (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) A2: u1 <= u1 "\/" u2 by Lm1; A3: u2 <= u1 "\/" u2 by Lm1; A4: u2 <= u2 "\/" u3 by Lm1; A5: u3 <= u2 "\/" u3 by Lm1; A6: u1 "\/" u2 <= (u1 "\/" u2) "\/" u3 by Lm1; A7: u3 <= (u1 "\/" u2) "\/" u3 by Lm1; A8: u1 <= (u1 "\/" u2) "\/" u3 by A1, A2, A6, ORDERS_2:3; u2 <= (u1 "\/" u2) "\/" u3 by A1, A3, A6, ORDERS_2:3; then A9: u2 "\/" u3 <= (u1 "\/" u2) "\/" u3 by A7, Lm1; now__::_thesis:_for_u4_being_Element_of_V_st_u1_<=_u4_&_u2_"\/"_u3_<=_u4_holds_ (u1_"\/"_u2)_"\/"_u3_<=_u4 let u4 be Element of V; ::_thesis: ( u1 <= u4 & u2 "\/" u3 <= u4 implies (u1 "\/" u2) "\/" u3 <= u4 ) assume that A10: u1 <= u4 and A11: u2 "\/" u3 <= u4 ; ::_thesis: (u1 "\/" u2) "\/" u3 <= u4 A12: u2 <= u4 by A1, A4, A11, ORDERS_2:3; A13: u3 <= u4 by A1, A5, A11, ORDERS_2:3; u1 "\/" u2 <= u4 by A10, A12, Lm1; hence (u1 "\/" u2) "\/" u3 <= u4 by A13, Lm1; ::_thesis: verum end; hence (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3) by A8, A9, Def13; ::_thesis: verum end; theorem Th15: :: LATTICE3:15 for N being antisymmetric with_infima RelStr for n1, n2 being Element of N holds n1 "/\" n2 = n2 "/\" n1 proof let N be antisymmetric with_infima RelStr ; ::_thesis: for n1, n2 being Element of N holds n1 "/\" n2 = n2 "/\" n1 let n1, n2 be Element of N; ::_thesis: n1 "/\" n2 = n2 "/\" n1 A1: n1 "/\" n2 <= n1 by Lm2; A2: n1 "/\" n2 <= n2 by Lm2; for n3 being Element of N st n3 <= n2 & n3 <= n1 holds n3 <= n1 "/\" n2 by Lm2; hence n1 "/\" n2 = n2 "/\" n1 by A1, A2, Def14; ::_thesis: verum end; theorem Th16: :: LATTICE3:16 for N being antisymmetric with_infima RelStr for n1, n2, n3 being Element of N st N is transitive holds (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3) proof let N be antisymmetric with_infima RelStr ; ::_thesis: for n1, n2, n3 being Element of N st N is transitive holds (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3) let n1, n2, n3 be Element of N; ::_thesis: ( N is transitive implies (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3) ) assume A1: N is transitive ; ::_thesis: (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3) A2: n1 "/\" n2 <= n1 by Lm2; A3: n1 "/\" n2 <= n2 by Lm2; A4: n2 "/\" n3 <= n2 by Lm2; A5: n2 "/\" n3 <= n3 by Lm2; A6: (n1 "/\" n2) "/\" n3 <= n1 "/\" n2 by Lm2; A7: (n1 "/\" n2) "/\" n3 <= n3 by Lm2; A8: (n1 "/\" n2) "/\" n3 <= n1 by A1, A2, A6, ORDERS_2:3; (n1 "/\" n2) "/\" n3 <= n2 by A1, A3, A6, ORDERS_2:3; then A9: (n1 "/\" n2) "/\" n3 <= n2 "/\" n3 by A7, Lm2; now__::_thesis:_for_n4_being_Element_of_N_st_n4_<=_n1_&_n4_<=_n2_"/\"_n3_holds_ n4_<=_(n1_"/\"_n2)_"/\"_n3 let n4 be Element of N; ::_thesis: ( n4 <= n1 & n4 <= n2 "/\" n3 implies n4 <= (n1 "/\" n2) "/\" n3 ) assume that A10: n4 <= n1 and A11: n4 <= n2 "/\" n3 ; ::_thesis: n4 <= (n1 "/\" n2) "/\" n3 A12: n4 <= n2 by A1, A4, A11, ORDERS_2:3; A13: n4 <= n3 by A1, A5, A11, ORDERS_2:3; n4 <= n1 "/\" n2 by A10, A12, Lm2; hence n4 <= (n1 "/\" n2) "/\" n3 by A13, Lm2; ::_thesis: verum end; hence (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3) by A8, A9, Def14; ::_thesis: verum end; definition let L be antisymmetric with_infima RelStr ; let x, y be Element of L; :: original: "/\" redefine funcx "/\" y -> Element of L; commutativity for x, y being Element of L holds x "/\" y = y "/\" x by Th15; end; definition let L be antisymmetric with_suprema RelStr ; let x, y be Element of L; :: original: "\/" redefine funcx "\/" y -> Element of L; commutativity for x, y being Element of L holds x "\/" y = y "\/" x by Th13; end; theorem Th17: :: LATTICE3:17 for K being reflexive antisymmetric with_suprema with_infima RelStr for k1, k2 being Element of K holds (k1 "/\" k2) "\/" k2 = k2 proof let K be reflexive antisymmetric with_suprema with_infima RelStr ; ::_thesis: for k1, k2 being Element of K holds (k1 "/\" k2) "\/" k2 = k2 let k1, k2 be Element of K; ::_thesis: (k1 "/\" k2) "\/" k2 = k2 A1: k1 "/\" k2 <= k2 by Lm2; A2: k2 <= k2 ; for k3 being Element of K st k1 "/\" k2 <= k3 & k2 <= k3 holds k2 <= k3 ; hence (k1 "/\" k2) "\/" k2 = k2 by A1, A2, Def13; ::_thesis: verum end; theorem Th18: :: LATTICE3:18 for K being reflexive antisymmetric with_suprema with_infima RelStr for k1, k2 being Element of K holds k1 "/\" (k1 "\/" k2) = k1 proof let K be reflexive antisymmetric with_suprema with_infima RelStr ; ::_thesis: for k1, k2 being Element of K holds k1 "/\" (k1 "\/" k2) = k1 let k1, k2 be Element of K; ::_thesis: k1 "/\" (k1 "\/" k2) = k1 A1: k1 <= k1 ; A2: k1 <= k1 "\/" k2 by Lm1; for k3 being Element of K st k3 <= k1 & k3 <= k1 "\/" k2 holds k3 <= k1 ; hence k1 "/\" (k1 "\/" k2) = k1 by A1, A2, Def14; ::_thesis: verum end; theorem Th19: :: LATTICE3:19 for A being with_suprema with_infima Poset ex L being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L proof let A be with_suprema with_infima Poset; ::_thesis: ex L being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L defpred S1[ Element of A, Element of A, set ] means for x9, y9 being Element of A st x9 = $1 & y9 = $2 holds $3 = x9 "\/" y9; A1: for x, y being Element of A ex u being Element of A st S1[x,y,u] proof let x, y be Element of A; ::_thesis: ex u being Element of A st S1[x,y,u] reconsider x9 = x, y9 = y as Element of A ; take x9 "\/" y9 ; ::_thesis: S1[x,y,x9 "\/" y9] thus S1[x,y,x9 "\/" y9] ; ::_thesis: verum end; consider j being BinOp of the carrier of A such that A2: for x, y being Element of A holds S1[x,y,j . (x,y)] from BINOP_1:sch_3(A1); defpred S2[ Element of A, Element of A, set ] means for x9, y9 being Element of A st x9 = $1 & y9 = $2 holds $3 = x9 "/\" y9; A3: for x, y being Element of A ex u being Element of A st S2[x,y,u] proof let x, y be Element of A; ::_thesis: ex u being Element of A st S2[x,y,u] reconsider x9 = x, y9 = y as Element of A ; take x9 "/\" y9 ; ::_thesis: S2[x,y,x9 "/\" y9] thus S2[x,y,x9 "/\" y9] ; ::_thesis: verum end; consider m being BinOp of the carrier of A such that A4: for x, y being Element of A holds S2[x,y,m . (x,y)] from BINOP_1:sch_3(A3); set L = LattStr(# the carrier of A,j,m #); A5: now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_A,j,m_#)_holds_a_"\/"_b_=_b_"\/"_a let a, b be Element of LattStr(# the carrier of A,j,m #); ::_thesis: a "\/" b = b "\/" a reconsider x = a, y = b as Element of A ; j . (x,y) = x "\/" y by A2; hence a "\/" b = b "\/" a by A2; ::_thesis: verum end; A6: now__::_thesis:_for_a,_b,_c_being_Element_of_LattStr(#_the_carrier_of_A,j,m_#)_holds_a_"\/"_(b_"\/"_c)_=_(a_"\/"_b)_"\/"_c let a, b, c be Element of LattStr(# the carrier of A,j,m #); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c reconsider x = a, y = b, z = c as Element of A ; thus a "\/" (b "\/" c) = j . (x,(y "\/" z)) by A2 .= x "\/" (y "\/" z) by A2 .= (x "\/" y) "\/" z by Th14 .= j . ((x "\/" y),z) by A2 .= (a "\/" b) "\/" c by A2 ; ::_thesis: verum end; A7: now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_A,j,m_#)_holds_(a_"/\"_b)_"\/"_b_=_b let a, b be Element of LattStr(# the carrier of A,j,m #); ::_thesis: (a "/\" b) "\/" b = b reconsider x = a, y = b as Element of A ; thus (a "/\" b) "\/" b = j . ((x "/\" y),y) by A4 .= (x "/\" y) "\/" y by A2 .= b by Th17 ; ::_thesis: verum end; A8: now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_A,j,m_#)_holds_a_"/\"_b_=_b_"/\"_a let a, b be Element of LattStr(# the carrier of A,j,m #); ::_thesis: a "/\" b = b "/\" a reconsider x = a, y = b as Element of A ; m . (x,y) = x "/\" y by A4; hence a "/\" b = b "/\" a by A4; ::_thesis: verum end; A9: now__::_thesis:_for_a,_b,_c_being_Element_of_LattStr(#_the_carrier_of_A,j,m_#)_holds_a_"/\"_(b_"/\"_c)_=_(a_"/\"_b)_"/\"_c let a, b, c be Element of LattStr(# the carrier of A,j,m #); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c reconsider x = a, y = b, z = c as Element of A ; thus a "/\" (b "/\" c) = m . (x,(y "/\" z)) by A4 .= x "/\" (y "/\" z) by A4 .= (x "/\" y) "/\" z by Th16 .= m . ((x "/\" y),z) by A4 .= (a "/\" b) "/\" c by A4 ; ::_thesis: verum end; now__::_thesis:_for_a,_b_being_Element_of_LattStr(#_the_carrier_of_A,j,m_#)_holds_a_"/\"_(a_"\/"_b)_=_a let a, b be Element of LattStr(# the carrier of A,j,m #); ::_thesis: a "/\" (a "\/" b) = a reconsider x = a, y = b as Element of A ; thus a "/\" (a "\/" b) = m . (x,(x "\/" y)) by A2 .= x "/\" (x "\/" y) by A4 .= a by Th18 ; ::_thesis: verum end; then ( LattStr(# the carrier of A,j,m #) is join-commutative & LattStr(# the carrier of A,j,m #) is join-associative & LattStr(# the carrier of A,j,m #) is meet-absorbing & LattStr(# the carrier of A,j,m #) is meet-commutative & LattStr(# the carrier of A,j,m #) is meet-associative & LattStr(# the carrier of A,j,m #) is join-absorbing ) by A5, A6, A7, A8, A9, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; then reconsider L = LattStr(# the carrier of A,j,m #) as strict Lattice ; take L ; ::_thesis: RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L A10: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def_8; LattRel L = the InternalRel of A proof let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in LattRel L or [x,y] in the InternalRel of A ) & ( not [x,y] in the InternalRel of A or [x,y] in LattRel L ) ) thus ( [x,y] in LattRel L implies [x,y] in the InternalRel of A ) ::_thesis: ( not [x,y] in the InternalRel of A or [x,y] in LattRel L ) proof assume [x,y] in LattRel L ; ::_thesis: [x,y] in the InternalRel of A then consider p, q being Element of L such that A11: [x,y] = [p,q] and A12: p [= q by A10; reconsider p9 = p, q9 = q as Element of A ; p9 "\/" q9 = p "\/" q by A2 .= q by A12, LATTICES:def_3 ; then p9 <= q9 by Lm1; hence [x,y] in the InternalRel of A by A11, ORDERS_2:def_5; ::_thesis: verum end; assume A13: [x,y] in the InternalRel of A ; ::_thesis: [x,y] in LattRel L then consider x1, x2 being set such that A14: x1 in the carrier of A and A15: x2 in the carrier of A and A16: [x,y] = [x1,x2] by ZFMISC_1:84; reconsider x1 = x1, x2 = x2 as Element of A by A14, A15; reconsider y1 = x1, y2 = x2 as Element of L ; A17: x1 <= x2 by A13, A16, ORDERS_2:def_5; x2 <= x2 ; then A18: x1 "\/" x2 <= x2 by A17, Lm1; x2 <= x1 "\/" x2 by Lm1; then x2 = x1 "\/" x2 by A18, ORDERS_2:2 .= y1 "\/" y2 by A2 ; then y1 [= y2 by LATTICES:def_3; hence [x,y] in LattRel L by A10, A16; ::_thesis: verum end; hence RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L ; ::_thesis: verum end; definition let A be RelStr ; assume A1: A is with_suprema with_infima Poset ; func latt A -> strict Lattice means :Def15: :: LATTICE3:def 15 RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet it; existence ex b1 being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b1 by A1, Th19; uniqueness for b1, b2 being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b1 & RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b2 holds b1 = b2 by Th6; end; :: deftheorem Def15 defines latt LATTICE3:def_15_:_ for A being RelStr st A is with_suprema with_infima Poset holds for b2 being strict Lattice holds ( b2 = latt A iff RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b2 ); theorem :: LATTICE3:20 for L being Lattice holds ( (LattRel L) ~ = LattRel (L .:) & (LattPOSet L) ~ = LattPOSet (L .:) ) proof let L be Lattice; ::_thesis: ( (LattRel L) ~ = LattRel (L .:) & (LattPOSet L) ~ = LattPOSet (L .:) ) A1: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def_8; A2: LattRel (L .:) = { [p9,q9] where p9, q9 is Element of (L .:) : p9 [= q9 } by FILTER_1:def_8; A3: L .: = LattStr(# H1(L),H3(L),H2(L) #) by LATTICE2:def_2; thus (LattRel L) ~ = LattRel (L .:) ::_thesis: (LattPOSet L) ~ = LattPOSet (L .:) proof let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in (LattRel L) ~ or [x,y] in LattRel (L .:) ) & ( not [x,y] in LattRel (L .:) or [x,y] in (LattRel L) ~ ) ) thus ( [x,y] in (LattRel L) ~ implies [x,y] in LattRel (L .:) ) ::_thesis: ( not [x,y] in LattRel (L .:) or [x,y] in (LattRel L) ~ ) proof assume [x,y] in (LattRel L) ~ ; ::_thesis: [x,y] in LattRel (L .:) then [y,x] in LattRel L by RELAT_1:def_7; then consider p, q being Element of L such that A4: [y,x] = [p,q] and A5: p [= q by A1; reconsider p9 = p, q9 = q as Element of (L .:) by A3; A6: x = q by A4, XTUPLE_0:1; A7: y = p by A4, XTUPLE_0:1; q9 [= p9 by A5, LATTICE2:38; hence [x,y] in LattRel (L .:) by A2, A6, A7; ::_thesis: verum end; assume [x,y] in LattRel (L .:) ; ::_thesis: [x,y] in (LattRel L) ~ then consider p9, q9 being Element of (L .:) such that A8: [x,y] = [p9,q9] and A9: p9 [= q9 by A2; reconsider p = p9, q = q9 as Element of L by A3; A10: x = p by A8, XTUPLE_0:1; A11: y = q by A8, XTUPLE_0:1; q [= p by A9, LATTICE2:39; then [y,x] in LattRel L by A1, A10, A11; hence [x,y] in (LattRel L) ~ by RELAT_1:def_7; ::_thesis: verum end; hence (LattPOSet L) ~ = LattPOSet (L .:) by A3; ::_thesis: verum end; begin definition let L be non empty LattStr ; let p be Element of L; let X be set ; predp is_less_than X means :Def16: :: LATTICE3:def 16 for q being Element of L st q in X holds p [= q; predX is_less_than p means :Def17: :: LATTICE3:def 17 for q being Element of L st q in X holds q [= p; end; :: deftheorem Def16 defines is_less_than LATTICE3:def_16_:_ for L being non empty LattStr for p being Element of L for X being set holds ( p is_less_than X iff for q being Element of L st q in X holds p [= q ); :: deftheorem Def17 defines is_less_than LATTICE3:def_17_:_ for L being non empty LattStr for p being Element of L for X being set holds ( X is_less_than p iff for q being Element of L st q in X holds q [= p ); notation let L be non empty LattStr ; let p be Element of L; let X be set ; synonym X is_greater_than p for p is_less_than X; synonym p is_greater_than X for X is_less_than p; end; theorem :: LATTICE3:21 for L being Lattice for p, q, r being Element of L holds ( p is_less_than {q,r} iff p [= q "/\" r ) proof let L be Lattice; ::_thesis: for p, q, r being Element of L holds ( p is_less_than {q,r} iff p [= q "/\" r ) let p, q, r be Element of L; ::_thesis: ( p is_less_than {q,r} iff p [= q "/\" r ) A1: q in {q,r} by TARSKI:def_2; A2: r in {q,r} by TARSKI:def_2; thus ( p is_less_than {q,r} implies p [= q "/\" r ) ::_thesis: ( p [= q "/\" r implies p is_less_than {q,r} ) proof assume A3: p is_less_than {q,r} ; ::_thesis: p [= q "/\" r then A4: p [= q by A1, Def16; p [= r by A2, A3, Def16; hence p [= q "/\" r by A4, FILTER_0:7; ::_thesis: verum end; assume A5: p [= q "/\" r ; ::_thesis: p is_less_than {q,r} let a be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( a in {q,r} implies p [= a ) assume a in {q,r} ; ::_thesis: p [= a then A6: ( a = q or a = r ) by TARSKI:def_2; A7: q "/\" r [= q by LATTICES:6; r "/\" q [= r by LATTICES:6; hence p [= a by A5, A6, A7, LATTICES:7; ::_thesis: verum end; theorem :: LATTICE3:22 for L being Lattice for p, q, r being Element of L holds ( p is_greater_than {q,r} iff q "\/" r [= p ) proof let L be Lattice; ::_thesis: for p, q, r being Element of L holds ( p is_greater_than {q,r} iff q "\/" r [= p ) let p, q, r be Element of L; ::_thesis: ( p is_greater_than {q,r} iff q "\/" r [= p ) A1: q in {q,r} by TARSKI:def_2; A2: r in {q,r} by TARSKI:def_2; thus ( p is_greater_than {q,r} implies q "\/" r [= p ) ::_thesis: ( q "\/" r [= p implies p is_greater_than {q,r} ) proof assume A3: p is_greater_than {q,r} ; ::_thesis: q "\/" r [= p then A4: q [= p by A1, Def17; r [= p by A2, A3, Def17; hence q "\/" r [= p by A4, FILTER_0:6; ::_thesis: verum end; assume A5: q "\/" r [= p ; ::_thesis: p is_greater_than {q,r} let a be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( a in {q,r} implies a [= p ) assume a in {q,r} ; ::_thesis: a [= p then A6: ( a = q or a = r ) by TARSKI:def_2; A7: q [= q "\/" r by LATTICES:5; r [= r "\/" q by LATTICES:5; hence a [= p by A5, A6, A7, LATTICES:7; ::_thesis: verum end; definition let IT be non empty LattStr ; attrIT is complete means :Def18: :: LATTICE3:def 18 for X being set ex p being Element of IT st ( X is_less_than p & ( for r being Element of IT st X is_less_than r holds p [= r ) ); attrIT is \/-distributive means :Def19: :: LATTICE3:def 19 for X being set for a, b, c being Element of IT st X is_less_than a & ( for d being Element of IT st X is_less_than d holds a [= d ) & { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than c & ( for d being Element of IT st { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than d holds c [= d ) holds b "/\" a [= c; attrIT is /\-distributive means :: LATTICE3:def 20 for X being set for a, b, c being Element of IT st X is_greater_than a & ( for d being Element of IT st X is_greater_than d holds d [= a ) & { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than c & ( for d being Element of IT st { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than d holds d [= c ) holds c [= b "\/" a; end; :: deftheorem Def18 defines complete LATTICE3:def_18_:_ for IT being non empty LattStr holds ( IT is complete iff for X being set ex p being Element of IT st ( X is_less_than p & ( for r being Element of IT st X is_less_than r holds p [= r ) ) ); :: deftheorem Def19 defines \/-distributive LATTICE3:def_19_:_ for IT being non empty LattStr holds ( IT is \/-distributive iff for X being set for a, b, c being Element of IT st X is_less_than a & ( for d being Element of IT st X is_less_than d holds a [= d ) & { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than c & ( for d being Element of IT st { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than d holds c [= d ) holds b "/\" a [= c ); :: deftheorem defines /\-distributive LATTICE3:def_20_:_ for IT being non empty LattStr holds ( IT is /\-distributive iff for X being set for a, b, c being Element of IT st X is_greater_than a & ( for d being Element of IT st X is_greater_than d holds d [= a ) & { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than c & ( for d being Element of IT st { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than d holds d [= c ) holds c [= b "\/" a ); theorem :: LATTICE3:23 for X being set for B being B_Lattice for a being Element of B holds ( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` ) proof let X be set ; ::_thesis: for B being B_Lattice for a being Element of B holds ( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` ) let B be B_Lattice; ::_thesis: for a being Element of B holds ( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` ) let a be Element of B; ::_thesis: ( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` ) set Y = { (b `) where b is Element of B : b in X } ; thus ( X is_less_than a implies { (b `) where b is Element of B : b in X } is_greater_than a ` ) ::_thesis: ( { (b `) where b is Element of B : b in X } is_greater_than a ` implies X is_less_than a ) proof assume A1: for b being Element of B st b in X holds b [= a ; :: according to LATTICE3:def_17 ::_thesis: { (b `) where b is Element of B : b in X } is_greater_than a ` let b be Element of B; :: according to LATTICE3:def_16 ::_thesis: ( b in { (b `) where b is Element of B : b in X } implies a ` [= b ) assume b in { (b `) where b is Element of B : b in X } ; ::_thesis: a ` [= b then ex c being Element of B st ( b = c ` & c in X ) ; hence a ` [= b by A1, LATTICES:26; ::_thesis: verum end; assume A2: for b being Element of B st b in { (b `) where b is Element of B : b in X } holds a ` [= b ; :: according to LATTICE3:def_16 ::_thesis: X is_less_than a let b be Element of B; :: according to LATTICE3:def_17 ::_thesis: ( b in X implies b [= a ) assume b in X ; ::_thesis: b [= a then A3: b ` in { (b `) where b is Element of B : b in X } ; A4: (a `) ` = a ; (b `) ` = b ; hence b [= a by A2, A3, A4, LATTICES:26; ::_thesis: verum end; theorem Th24: :: LATTICE3:24 for X being set for B being B_Lattice for a being Element of B holds ( X is_greater_than a iff { (b `) where b is Element of B : b in X } is_less_than a ` ) proof let X be set ; ::_thesis: for B being B_Lattice for a being Element of B holds ( X is_greater_than a iff { (b `) where b is Element of B : b in X } is_less_than a ` ) let B be B_Lattice; ::_thesis: for a being Element of B holds ( X is_greater_than a iff { (b `) where b is Element of B : b in X } is_less_than a ` ) let a be Element of B; ::_thesis: ( X is_greater_than a iff { (b `) where b is Element of B : b in X } is_less_than a ` ) set Y = { (b `) where b is Element of B : b in X } ; thus ( X is_greater_than a implies { (b `) where b is Element of B : b in X } is_less_than a ` ) ::_thesis: ( { (b `) where b is Element of B : b in X } is_less_than a ` implies X is_greater_than a ) proof assume A1: for b being Element of B st b in X holds a [= b ; :: according to LATTICE3:def_16 ::_thesis: { (b `) where b is Element of B : b in X } is_less_than a ` let b be Element of B; :: according to LATTICE3:def_17 ::_thesis: ( b in { (b `) where b is Element of B : b in X } implies b [= a ` ) assume b in { (b `) where b is Element of B : b in X } ; ::_thesis: b [= a ` then ex c being Element of B st ( b = c ` & c in X ) ; hence b [= a ` by A1, LATTICES:26; ::_thesis: verum end; assume A2: for b being Element of B st b in { (b `) where b is Element of B : b in X } holds b [= a ` ; :: according to LATTICE3:def_17 ::_thesis: X is_greater_than a let b be Element of B; :: according to LATTICE3:def_16 ::_thesis: ( b in X implies a [= b ) assume b in X ; ::_thesis: a [= b then A3: b ` in { (b `) where b is Element of B : b in X } ; A4: (a `) ` = a ; (b `) ` = b ; hence a [= b by A2, A3, A4, LATTICES:26; ::_thesis: verum end; theorem Th25: :: LATTICE3:25 for X being set holds BooleLatt X is complete proof let X be set ; ::_thesis: BooleLatt X is complete set B = BooleLatt X; let x be set ; :: according to LATTICE3:def_18 ::_thesis: ex p being Element of (BooleLatt X) st ( x is_less_than p & ( for r being Element of (BooleLatt X) st x is_less_than r holds p [= r ) ) set p = union (x /\ (bool X)); A1: H1( BooleLatt X) = bool X by Def1; reconsider p = union (x /\ (bool X)) as Element of (BooleLatt X) by Def1; take p ; ::_thesis: ( x is_less_than p & ( for r being Element of (BooleLatt X) st x is_less_than r holds p [= r ) ) thus x is_less_than p ::_thesis: for r being Element of (BooleLatt X) st x is_less_than r holds p [= r proof let q be Element of (BooleLatt X); :: according to LATTICE3:def_17 ::_thesis: ( q in x implies q [= p ) assume q in x ; ::_thesis: q [= p then q in x /\ (bool X) by A1, XBOOLE_0:def_4; then q c= p by ZFMISC_1:74; hence q [= p by Th2; ::_thesis: verum end; let r be Element of (BooleLatt X); ::_thesis: ( x is_less_than r implies p [= r ) assume A2: for q being Element of (BooleLatt X) st q in x holds q [= r ; :: according to LATTICE3:def_17 ::_thesis: p [= r now__::_thesis:_for_z_being_set_st_z_in_x_/\_(bool_X)_holds_ z_c=_r let z be set ; ::_thesis: ( z in x /\ (bool X) implies z c= r ) assume A3: z in x /\ (bool X) ; ::_thesis: z c= r then A4: z in x by XBOOLE_0:def_4; reconsider z9 = z as Element of (BooleLatt X) by A1, A3; z9 [= r by A2, A4; hence z c= r by Th2; ::_thesis: verum end; then p c= r by ZFMISC_1:76; hence p [= r by Th2; ::_thesis: verum end; registration let X be set ; cluster BooleLatt X -> strict complete ; coherence BooleLatt X is complete by Th25; end; theorem Th26: :: LATTICE3:26 for X being set holds BooleLatt X is \/-distributive proof let X be set ; ::_thesis: BooleLatt X is \/-distributive let x be set ; :: according to LATTICE3:def_19 ::_thesis: for a, b, c being Element of (BooleLatt X) st x is_less_than a & ( for d being Element of (BooleLatt X) st x is_less_than d holds a [= d ) & { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than c & ( for d being Element of (BooleLatt X) st { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than d holds c [= d ) holds b "/\" a [= c set B = BooleLatt X; let a, b, c be Element of (BooleLatt X); ::_thesis: ( x is_less_than a & ( for d being Element of (BooleLatt X) st x is_less_than d holds a [= d ) & { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than c & ( for d being Element of (BooleLatt X) st { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than d holds c [= d ) implies b "/\" a [= c ) assume that A1: x is_less_than a and A2: for d being Element of (BooleLatt X) st x is_less_than d holds a [= d and A3: { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than c and A4: for d being Element of (BooleLatt X) st { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than d holds c [= d ; ::_thesis: b "/\" a [= c set Y = { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } ; A5: H1( BooleLatt X) = bool X by Def1; A6: { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } c= bool X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } or z in bool X ) assume z in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } ; ::_thesis: z in bool X then ex a9 being Element of (BooleLatt X) st ( z = b "/\" a9 & a9 in x ) ; hence z in bool X by A5; ::_thesis: verum end; A7: union { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } c= union (bool X) by A6, ZFMISC_1:77; union (bool X) = X by ZFMISC_1:81; then reconsider p = union (x /\ (bool X)), q = union { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } as Element of (BooleLatt X) by A7, Def1; now__::_thesis:_for_y_being_set_st_y_in_x_/\_(bool_X)_holds_ y_c=_a let y be set ; ::_thesis: ( y in x /\ (bool X) implies y c= a ) assume A8: y in x /\ (bool X) ; ::_thesis: y c= a then A9: y in x by XBOOLE_0:def_4; reconsider y9 = y as Element of (BooleLatt X) by A5, A8; y9 [= a by A1, A9, Def17; hence y c= a by Th2; ::_thesis: verum end; then A10: p c= a by ZFMISC_1:76; A11: x is_less_than p proof let q be Element of (BooleLatt X); :: according to LATTICE3:def_17 ::_thesis: ( q in x implies q [= p ) assume q in x ; ::_thesis: q [= p then q in x /\ (bool X) by A5, XBOOLE_0:def_4; then q c= p by ZFMISC_1:74; hence q [= p by Th2; ::_thesis: verum end; A12: p [= a by A10, Th2; a [= p by A2, A11; then A13: a = p by A12, LATTICES:8; now__::_thesis:_for_y_being_set_st_y_in__{__(b_"/\"_a9)_where_a9_is_Element_of_(BooleLatt_X)_:_a9_in_x__}__holds_ y_c=_c let y be set ; ::_thesis: ( y in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } implies y c= c ) assume A14: y in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } ; ::_thesis: y c= c then consider a9 being Element of (BooleLatt X) such that A15: y = b "/\" a9 and a9 in x ; b "/\" a9 [= c by A3, A14, A15, Def17; hence y c= c by A15, Th2; ::_thesis: verum end; then A16: q c= c by ZFMISC_1:76; A17: { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_less_than q proof let p be Element of (BooleLatt X); :: according to LATTICE3:def_17 ::_thesis: ( p in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } implies p [= q ) assume p in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } ; ::_thesis: p [= q then p c= q by ZFMISC_1:74; hence p [= q by Th2; ::_thesis: verum end; A18: q [= c by A16, Th2; c [= q by A4, A17; then A19: c = q by A18, LATTICES:8; b /\ a c= c proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in b /\ a or z in c ) assume A20: z in b /\ a ; ::_thesis: z in c then A21: z in b by XBOOLE_0:def_4; z in a by A20, XBOOLE_0:def_4; then consider y being set such that A22: z in y and A23: y in x /\ (bool X) by A13, TARSKI:def_4; A24: y in x by A23, XBOOLE_0:def_4; reconsider y = y as Element of (BooleLatt X) by A5, A23; A25: b "/\" y in { (b "/\" a9) where a9 is Element of (BooleLatt X) : a9 in x } by A24; z in b /\ y by A21, A22, XBOOLE_0:def_4; hence z in c by A19, A25, TARSKI:def_4; ::_thesis: verum end; hence b "/\" a [= c by Th2; ::_thesis: verum end; theorem Th27: :: LATTICE3:27 for X being set holds BooleLatt X is /\-distributive proof let X be set ; ::_thesis: BooleLatt X is /\-distributive let x be set ; :: according to LATTICE3:def_20 ::_thesis: for a, b, c being Element of (BooleLatt X) st x is_greater_than a & ( for d being Element of (BooleLatt X) st x is_greater_than d holds d [= a ) & { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than c & ( for d being Element of (BooleLatt X) st { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than d holds d [= c ) holds c [= b "\/" a set B = BooleLatt X; let a, b, c be Element of (BooleLatt X); ::_thesis: ( x is_greater_than a & ( for d being Element of (BooleLatt X) st x is_greater_than d holds d [= a ) & { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than c & ( for d being Element of (BooleLatt X) st { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than d holds d [= c ) implies c [= b "\/" a ) assume that A1: x is_greater_than a and A2: for d being Element of (BooleLatt X) st x is_greater_than d holds d [= a and A3: { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than c and A4: for d being Element of (BooleLatt X) st { (b "\/" a9) where a9 is Element of (BooleLatt X) : a9 in x } is_greater_than d holds d [= c ; ::_thesis: c [= b "\/" a set x9 = { (e `) where e is Element of (BooleLatt X) : e in x } ; set y = { (b "\/" e) where e is Element of (BooleLatt X) : e in x } ; set y9 = { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } ; set z = { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } ; A5: { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } = { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } proof thus { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } c= { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } :: according to XBOOLE_0:def_10 ::_thesis: { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } c= { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } or s in { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } ) assume s in { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } ; ::_thesis: s in { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } then consider e being Element of (BooleLatt X) such that A6: s = (b `) "/\" e and A7: e in { (e `) where e is Element of (BooleLatt X) : e in x } ; consider i being Element of (BooleLatt X) such that A8: e = i ` and A9: i in x by A7; A10: b "\/" i in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } by A9; (b "\/" i) ` = s by A6, A8, LATTICES:24; hence s in { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } by A10; ::_thesis: verum end; let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } or s in { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } ) assume s in { (e `) where e is Element of (BooleLatt X) : e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } } ; ::_thesis: s in { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } then consider e being Element of (BooleLatt X) such that A11: s = e ` and A12: e in { (b "\/" e) where e is Element of (BooleLatt X) : e in x } ; consider i being Element of (BooleLatt X) such that A13: e = b "\/" i and A14: i in x by A12; A15: i ` in { (e `) where e is Element of (BooleLatt X) : e in x } by A14; s = (b `) "/\" (i `) by A11, A13, LATTICES:24; hence s in { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } by A15; ::_thesis: verum end; A18: (c `) ` = c ; A19: { (e `) where e is Element of (BooleLatt X) : e in x } is_less_than a ` by A1, Th24; A20: for d being Element of (BooleLatt X) st { (e `) where e is Element of (BooleLatt X) : e in x } is_less_than d holds a ` [= d proof let d be Element of (BooleLatt X); ::_thesis: ( { (e `) where e is Element of (BooleLatt X) : e in x } is_less_than d implies a ` [= d ) A21: (d `) ` = d ; assume { (e `) where e is Element of (BooleLatt X) : e in x } is_less_than d ; ::_thesis: a ` [= d then x is_greater_than d ` by A21, Th24; hence a ` [= d by A2, A21, LATTICES:26; ::_thesis: verum end; A22: { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } is_less_than c ` by A3, A5, Th24; A23: for d being Element of (BooleLatt X) st { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } is_less_than d holds c ` [= d proof let d be Element of (BooleLatt X); ::_thesis: ( { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } is_less_than d implies c ` [= d ) A24: (d `) ` = d ; assume { ((b `) "/\" e) where e is Element of (BooleLatt X) : e in { (e `) where e is Element of (BooleLatt X) : e in x } } is_less_than d ; ::_thesis: c ` [= d then { (b "\/" e) where e is Element of (BooleLatt X) : e in x } is_greater_than d ` by A5, A24, Th24; hence c ` [= d by A4, A24, LATTICES:26; ::_thesis: verum end; BooleLatt X is \/-distributive by Th26; then A25: (b `) "/\" (a `) [= c ` by A19, A20, A22, A23, Def19; ((b `) "/\" (a `)) ` = ((b `) `) "\/" ((a `) `) by LATTICES:23; hence c [= b "\/" a by A18, A25, LATTICES:26; ::_thesis: verum end; registration cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete \/-distributive /\-distributive for LattStr ; existence ex b1 being Lattice st ( b1 is complete & b1 is \/-distributive & b1 is /\-distributive & b1 is strict ) proof set X = the set ; ( BooleLatt the set is complete & BooleLatt the set is \/-distributive & BooleLatt the set is /\-distributive ) by Th26, Th27; hence ex b1 being Lattice st ( b1 is complete & b1 is \/-distributive & b1 is /\-distributive & b1 is strict ) ; ::_thesis: verum end; end; theorem Th28: :: LATTICE3:28 for X being set for L being Lattice for p being Element of L holds ( p is_less_than X iff p % is_<=_than X ) proof let X be set ; ::_thesis: for L being Lattice for p being Element of L holds ( p is_less_than X iff p % is_<=_than X ) let L be Lattice; ::_thesis: for p being Element of L holds ( p is_less_than X iff p % is_<=_than X ) let p be Element of L; ::_thesis: ( p is_less_than X iff p % is_<=_than X ) thus ( p is_less_than X implies p % is_<=_than X ) ::_thesis: ( p % is_<=_than X implies p is_less_than X ) proof assume A1: for q being Element of L st q in X holds p [= q ; :: according to LATTICE3:def_16 ::_thesis: p % is_<=_than X let p9 be Element of (LattPOSet L); :: according to LATTICE3:def_8 ::_thesis: ( p9 in X implies p % <= p9 ) A2: (% p9) % = % p9 ; assume p9 in X ; ::_thesis: p % <= p9 then p [= % p9 by A1; hence p % <= p9 by A2, Th7; ::_thesis: verum end; assume A3: for q9 being Element of (LattPOSet L) st q9 in X holds p % <= q9 ; :: according to LATTICE3:def_8 ::_thesis: p is_less_than X let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( q in X implies p [= q ) assume q in X ; ::_thesis: p [= q then p % <= q % by A3; hence p [= q by Th7; ::_thesis: verum end; theorem :: LATTICE3:29 for X being set for L being Lattice for p9 being Element of (LattPOSet L) holds ( p9 is_<=_than X iff % p9 is_less_than X ) proof let X be set ; ::_thesis: for L being Lattice for p9 being Element of (LattPOSet L) holds ( p9 is_<=_than X iff % p9 is_less_than X ) let L be Lattice; ::_thesis: for p9 being Element of (LattPOSet L) holds ( p9 is_<=_than X iff % p9 is_less_than X ) let p9 be Element of (LattPOSet L); ::_thesis: ( p9 is_<=_than X iff % p9 is_less_than X ) (% p9) % = % p9 ; hence ( p9 is_<=_than X iff % p9 is_less_than X ) by Th28; ::_thesis: verum end; theorem Th30: :: LATTICE3:30 for X being set for L being Lattice for p being Element of L holds ( X is_less_than p iff X is_<=_than p % ) proof let X be set ; ::_thesis: for L being Lattice for p being Element of L holds ( X is_less_than p iff X is_<=_than p % ) let L be Lattice; ::_thesis: for p being Element of L holds ( X is_less_than p iff X is_<=_than p % ) let p be Element of L; ::_thesis: ( X is_less_than p iff X is_<=_than p % ) thus ( X is_less_than p implies X is_<=_than p % ) ::_thesis: ( X is_<=_than p % implies X is_less_than p ) proof assume A1: for q being Element of L st q in X holds q [= p ; :: according to LATTICE3:def_17 ::_thesis: X is_<=_than p % let p9 be Element of (LattPOSet L); :: according to LATTICE3:def_9 ::_thesis: ( p9 in X implies p9 <= p % ) A2: (% p9) % = % p9 ; assume p9 in X ; ::_thesis: p9 <= p % then % p9 [= p by A1; hence p9 <= p % by A2, Th7; ::_thesis: verum end; assume A3: for q9 being Element of (LattPOSet L) st q9 in X holds q9 <= p % ; :: according to LATTICE3:def_9 ::_thesis: X is_less_than p let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( q in X implies q [= p ) assume q in X ; ::_thesis: q [= p then q % <= p % by A3; hence q [= p by Th7; ::_thesis: verum end; theorem Th31: :: LATTICE3:31 for X being set for L being Lattice for p9 being Element of (LattPOSet L) holds ( X is_<=_than p9 iff X is_less_than % p9 ) proof let X be set ; ::_thesis: for L being Lattice for p9 being Element of (LattPOSet L) holds ( X is_<=_than p9 iff X is_less_than % p9 ) let L be Lattice; ::_thesis: for p9 being Element of (LattPOSet L) holds ( X is_<=_than p9 iff X is_less_than % p9 ) let p9 be Element of (LattPOSet L); ::_thesis: ( X is_<=_than p9 iff X is_less_than % p9 ) (% p9) % = % p9 ; hence ( X is_<=_than p9 iff X is_less_than % p9 ) by Th30; ::_thesis: verum end; registration let A be non empty complete Poset; cluster latt A -> strict complete ; coherence latt A is complete proof ( A is with_suprema & A is with_infima ) by Th12; then A1: RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet (latt A) by Def15; set B = LattPOSet (latt A); latt A is complete proof let X be set ; :: according to LATTICE3:def_18 ::_thesis: ex p being Element of (latt A) st ( X is_less_than p & ( for r being Element of (latt A) st X is_less_than r holds p [= r ) ) consider a being Element of A such that A2: X is_<=_than a and A3: for b being Element of A st X is_<=_than b holds a <= b by Def12; reconsider a9 = a as Element of (LattPOSet (latt A)) by A1; take p = % a9; ::_thesis: ( X is_less_than p & ( for r being Element of (latt A) st X is_less_than r holds p [= r ) ) A4: p % = p ; thus X is_less_than p ::_thesis: for r being Element of (latt A) st X is_less_than r holds p [= r proof let q be Element of (latt A); :: according to LATTICE3:def_17 ::_thesis: ( q in X implies q [= p ) reconsider b = q as Element of A by A1; assume q in X ; ::_thesis: q [= p then b <= a by A2, Def9; then [b,a] in the InternalRel of A by ORDERS_2:def_5; then q % <= a9 by A1, ORDERS_2:def_5; hence q [= p by A4, Th7; ::_thesis: verum end; let q be Element of (latt A); ::_thesis: ( X is_less_than q implies p [= q ) assume X is_less_than q ; ::_thesis: p [= q then A5: X is_<=_than q % by Th30; reconsider b = q % as Element of A by A1; X is_<=_than b proof let c be Element of A; :: according to LATTICE3:def_9 ::_thesis: ( c in X implies c <= b ) reconsider c9 = c as Element of (LattPOSet (latt A)) by A1; assume c in X ; ::_thesis: c <= b then c9 <= q % by A5, Def9; then [c,b] in the InternalRel of RelStr(# the carrier of A, the InternalRel of A #) by A1, ORDERS_2:def_5; hence c <= b by ORDERS_2:def_5; ::_thesis: verum end; then a <= b by A3; then [a,b] in the InternalRel of A by ORDERS_2:def_5; then a9 <= q % by A1, ORDERS_2:def_5; hence p [= q by A4, Th7; ::_thesis: verum end; hence latt A is complete ; ::_thesis: verum end; end; definition let L be non empty LattStr ; assume B1: L is complete Lattice ; let X be set ; func "\/" (X,L) -> Element of L means :Def21: :: LATTICE3:def 21 ( X is_less_than it & ( for r being Element of L st X is_less_than r holds it [= r ) ); existence ex b1 being Element of L st ( X is_less_than b1 & ( for r being Element of L st X is_less_than r holds b1 [= r ) ) by B1, Def18; uniqueness for b1, b2 being Element of L st X is_less_than b1 & ( for r being Element of L st X is_less_than r holds b1 [= r ) & X is_less_than b2 & ( for r being Element of L st X is_less_than r holds b2 [= r ) holds b1 = b2 proof let p1, p2 be Element of L; ::_thesis: ( X is_less_than p1 & ( for r being Element of L st X is_less_than r holds p1 [= r ) & X is_less_than p2 & ( for r being Element of L st X is_less_than r holds p2 [= r ) implies p1 = p2 ) assume that A1: X is_less_than p1 and A2: for r being Element of L st X is_less_than r holds p1 [= r and A3: X is_less_than p2 and A4: for r being Element of L st X is_less_than r holds p2 [= r ; ::_thesis: p1 = p2 A5: p1 [= p2 by A2, A3; p2 [= p1 by A1, A4; hence p1 = p2 by B1, A5, LATTICES:8; ::_thesis: verum end; end; :: deftheorem Def21 defines "\/" LATTICE3:def_21_:_ for L being non empty LattStr st L is complete Lattice holds for X being set for b3 being Element of L holds ( b3 = "\/" (X,L) iff ( X is_less_than b3 & ( for r being Element of L st X is_less_than r holds b3 [= r ) ) ); definition let L be non empty LattStr ; let X be set ; func "/\" (X,L) -> Element of L equals :: LATTICE3:def 22 "\/" ( { p where p is Element of L : p is_less_than X } ,L); correctness coherence "\/" ( { p where p is Element of L : p is_less_than X } ,L) is Element of L; ; end; :: deftheorem defines "/\" LATTICE3:def_22_:_ for L being non empty LattStr for X being set holds "/\" (X,L) = "\/" ( { p where p is Element of L : p is_less_than X } ,L); notation let L be non empty LattStr ; let X be Subset of L; synonym "\/" X for "\/" (X,L); synonym "/\" X for "/\" (X,L); end; theorem Th32: :: LATTICE3:32 for C being complete Lattice for a being Element of C for X being set holds "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C)) proof let C be complete Lattice; ::_thesis: for a being Element of C for X being set holds "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C)) let a be Element of C; ::_thesis: for X being set holds "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C)) let X be set ; ::_thesis: "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C)) set Y = { (a "/\" b) where b is Element of C : b in X } ; { (a "/\" b) where b is Element of C : b in X } is_less_than a "/\" ("\/" (X,C)) proof let c be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( c in { (a "/\" b) where b is Element of C : b in X } implies c [= a "/\" ("\/" (X,C)) ) assume c in { (a "/\" b) where b is Element of C : b in X } ; ::_thesis: c [= a "/\" ("\/" (X,C)) then consider b being Element of C such that A1: c = a "/\" b and A2: b in X ; X is_less_than "\/" (X,C) by Def21; then b [= "\/" (X,C) by A2, Def17; hence c [= a "/\" ("\/" (X,C)) by A1, LATTICES:9; ::_thesis: verum end; hence "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C)) by Def21; ::_thesis: verum end; theorem Th33: :: LATTICE3:33 for C being complete Lattice holds ( C is \/-distributive iff for X being set for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) ) proof let C be complete Lattice; ::_thesis: ( C is \/-distributive iff for X being set for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) ) thus ( C is \/-distributive implies for X being set for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) ) ::_thesis: ( ( for X being set for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) ) implies C is \/-distributive ) proof assume A1: for X being set for a, b, c being Element of C st X is_less_than a & ( for d being Element of C st X is_less_than d holds a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" b9) where b9 is Element of C : b9 in X } is_less_than d holds c [= d ) holds b "/\" a [= c ; :: according to LATTICE3:def_19 ::_thesis: for X being set for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) let X be set ; ::_thesis: for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) let a be Element of C; ::_thesis: a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) set Y = { (a "/\" b) where b is Element of C : b in X } ; A2: X is_less_than "\/" (X,C) by Def21; A3: for d being Element of C st X is_less_than d holds "\/" (X,C) [= d by Def21; A4: { (a "/\" b) where b is Element of C : b in X } is_less_than "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) by Def21; for d being Element of C st { (a "/\" b) where b is Element of C : b in X } is_less_than d holds "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= d by Def21; hence a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) by A1, A2, A3, A4; ::_thesis: verum end; assume A5: for X being set for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) ; ::_thesis: C is \/-distributive let X be set ; :: according to LATTICE3:def_19 ::_thesis: for a, b, c being Element of C st X is_less_than a & ( for d being Element of C st X is_less_than d holds a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than d holds c [= d ) holds b "/\" a [= c let a, b, c be Element of C; ::_thesis: ( X is_less_than a & ( for d being Element of C st X is_less_than d holds a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than d holds c [= d ) implies b "/\" a [= c ) assume A6: ( X is_less_than a & ( for d being Element of C st X is_less_than d holds a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" b9) where b9 is Element of C : b9 in X } is_less_than d holds c [= d ) ) ; ::_thesis: b "/\" a [= c then A7: a = "\/" (X,C) by Def21; c = "\/" ( { (b "/\" a9) where a9 is Element of C : a9 in X } ,C) by A6, Def21; hence b "/\" a [= c by A5, A7; ::_thesis: verum end; theorem Th34: :: LATTICE3:34 for C being complete Lattice for a being Element of C for X being set holds ( a = "/\" (X,C) iff ( a is_less_than X & ( for b being Element of C st b is_less_than X holds b [= a ) ) ) proof let C be complete Lattice; ::_thesis: for a being Element of C for X being set holds ( a = "/\" (X,C) iff ( a is_less_than X & ( for b being Element of C st b is_less_than X holds b [= a ) ) ) let a be Element of C; ::_thesis: for X being set holds ( a = "/\" (X,C) iff ( a is_less_than X & ( for b being Element of C st b is_less_than X holds b [= a ) ) ) let X be set ; ::_thesis: ( a = "/\" (X,C) iff ( a is_less_than X & ( for b being Element of C st b is_less_than X holds b [= a ) ) ) set Y = { b where b is Element of C : b is_less_than X } ; A1: ( a = "/\" (X,C) iff ( { b where b is Element of C : b is_less_than X } is_less_than a & ( for c being Element of C st { b where b is Element of C : b is_less_than X } is_less_than c holds a [= c ) ) ) by Def21; thus ( a = "/\" (X,C) implies ( a is_less_than X & ( for b being Element of C st b is_less_than X holds b [= a ) ) ) ::_thesis: ( a is_less_than X & ( for b being Element of C st b is_less_than X holds b [= a ) implies a = "/\" (X,C) ) proof assume A2: a = "/\" (X,C) ; ::_thesis: ( a is_less_than X & ( for b being Element of C st b is_less_than X holds b [= a ) ) then A3: { b where b is Element of C : b is_less_than X } is_less_than a by Def21; thus a is_less_than X ::_thesis: for b being Element of C st b is_less_than X holds b [= a proof let b be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( b in X implies a [= b ) assume A4: b in X ; ::_thesis: a [= b { b where b is Element of C : b is_less_than X } is_less_than b proof let c be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( c in { b where b is Element of C : b is_less_than X } implies c [= b ) assume c in { b where b is Element of C : b is_less_than X } ; ::_thesis: c [= b then ex d being Element of C st ( c = d & d is_less_than X ) ; hence c [= b by A4, Def16; ::_thesis: verum end; hence a [= b by A2, Def21; ::_thesis: verum end; let b be Element of C; ::_thesis: ( b is_less_than X implies b [= a ) assume b is_less_than X ; ::_thesis: b [= a then b in { b where b is Element of C : b is_less_than X } ; hence b [= a by A3, Def17; ::_thesis: verum end; assume that A5: a is_less_than X and A6: for b being Element of C st b is_less_than X holds b [= a ; ::_thesis: a = "/\" (X,C) A7: { b where b is Element of C : b is_less_than X } is_less_than a proof let b be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( b in { b where b is Element of C : b is_less_than X } implies b [= a ) assume b in { b where b is Element of C : b is_less_than X } ; ::_thesis: b [= a then ex c being Element of C st ( b = c & c is_less_than X ) ; hence b [= a by A6; ::_thesis: verum end; a in { b where b is Element of C : b is_less_than X } by A5; hence a = "/\" (X,C) by A1, A7, Def17; ::_thesis: verum end; theorem Th35: :: LATTICE3:35 for C being complete Lattice for a being Element of C for X being set holds a "\/" ("/\" (X,C)) [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) proof let C be complete Lattice; ::_thesis: for a being Element of C for X being set holds a "\/" ("/\" (X,C)) [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) let a be Element of C; ::_thesis: for X being set holds a "\/" ("/\" (X,C)) [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) let X be set ; ::_thesis: a "\/" ("/\" (X,C)) [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) set Y = { (a "\/" b) where b is Element of C : b in X } ; { (a "\/" b) where b is Element of C : b in X } is_greater_than a "\/" ("/\" (X,C)) proof let c be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( c in { (a "\/" b) where b is Element of C : b in X } implies a "\/" ("/\" (X,C)) [= c ) assume c in { (a "\/" b) where b is Element of C : b in X } ; ::_thesis: a "\/" ("/\" (X,C)) [= c then consider b being Element of C such that A1: c = a "\/" b and A2: b in X ; X is_greater_than "/\" (X,C) by Th34; then "/\" (X,C) [= b by A2, Def16; hence a "\/" ("/\" (X,C)) [= c by A1, FILTER_0:1; ::_thesis: verum end; hence a "\/" ("/\" (X,C)) [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) by Th34; ::_thesis: verum end; theorem Th36: :: LATTICE3:36 for C being complete Lattice holds ( C is /\-distributive iff for X being set for a being Element of C holds "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) ) proof let C be complete Lattice; ::_thesis: ( C is /\-distributive iff for X being set for a being Element of C holds "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) ) thus ( C is /\-distributive implies for X being set for a being Element of C holds "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) ) ::_thesis: ( ( for X being set for a being Element of C holds "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) ) implies C is /\-distributive ) proof assume A1: for X being set for a, b, c being Element of C st X is_greater_than a & ( for d being Element of C st X is_greater_than d holds d [= a ) & { (b "\/" a9) where a9 is Element of C : a9 in X } is_greater_than c & ( for d being Element of C st { (b "\/" b9) where b9 is Element of C : b9 in X } is_greater_than d holds d [= c ) holds c [= b "\/" a ; :: according to LATTICE3:def_20 ::_thesis: for X being set for a being Element of C holds "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) let X be set ; ::_thesis: for a being Element of C holds "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) let a be Element of C; ::_thesis: "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) set Y = { (a "\/" b) where b is Element of C : b in X } ; A2: X is_greater_than "/\" (X,C) by Th34; A3: for d being Element of C st X is_greater_than d holds d [= "/\" (X,C) by Th34; A4: { (a "\/" b) where b is Element of C : b in X } is_greater_than "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) by Th34; for d being Element of C st { (a "\/" b) where b is Element of C : b in X } is_greater_than d holds d [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) by Th34; hence "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) by A1, A2, A3, A4; ::_thesis: verum end; assume A5: for X being set for a being Element of C holds "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) ; ::_thesis: C is /\-distributive let X be set ; :: according to LATTICE3:def_20 ::_thesis: for a, b, c being Element of C st X is_greater_than a & ( for d being Element of C st X is_greater_than d holds d [= a ) & { (b "\/" a9) where a9 is Element of C : a9 in X } is_greater_than c & ( for d being Element of C st { (b "\/" a9) where a9 is Element of C : a9 in X } is_greater_than d holds d [= c ) holds c [= b "\/" a let a, b, c be Element of C; ::_thesis: ( X is_greater_than a & ( for d being Element of C st X is_greater_than d holds d [= a ) & { (b "\/" a9) where a9 is Element of C : a9 in X } is_greater_than c & ( for d being Element of C st { (b "\/" a9) where a9 is Element of C : a9 in X } is_greater_than d holds d [= c ) implies c [= b "\/" a ) assume A6: ( X is_greater_than a & ( for d being Element of C st X is_greater_than d holds d [= a ) & { (b "\/" a9) where a9 is Element of C : a9 in X } is_greater_than c & ( for d being Element of C st { (b "\/" b9) where b9 is Element of C : b9 in X } is_greater_than d holds d [= c ) ) ; ::_thesis: c [= b "\/" a then A7: a = "/\" (X,C) by Th34; c = "/\" ( { (b "\/" a9) where a9 is Element of C : a9 in X } ,C) by A6, Th34; hence c [= b "\/" a by A5, A7; ::_thesis: verum end; theorem :: LATTICE3:37 for C being complete Lattice for X being set holds "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C) proof let C be complete Lattice; ::_thesis: for X being set holds "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C) let X be set ; ::_thesis: "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C) set Y = { a where a is Element of C : a is_greater_than X } ; A1: "\/" (X,C) is_less_than { a where a is Element of C : a is_greater_than X } proof let a be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( a in { a where a is Element of C : a is_greater_than X } implies "\/" (X,C) [= a ) assume a in { a where a is Element of C : a is_greater_than X } ; ::_thesis: "\/" (X,C) [= a then ex b being Element of C st ( a = b & b is_greater_than X ) ; hence "\/" (X,C) [= a by Def21; ::_thesis: verum end; X is_less_than "\/" (X,C) by Def21; then "\/" (X,C) in { a where a is Element of C : a is_greater_than X } ; then for b being Element of C st b is_less_than { a where a is Element of C : a is_greater_than X } holds b [= "\/" (X,C) by Def16; hence "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C) by A1, Th34; ::_thesis: verum end; theorem Th38: :: LATTICE3:38 for C being complete Lattice for a being Element of C for X being set st a in X holds ( a [= "\/" (X,C) & "/\" (X,C) [= a ) proof let C be complete Lattice; ::_thesis: for a being Element of C for X being set st a in X holds ( a [= "\/" (X,C) & "/\" (X,C) [= a ) let a be Element of C; ::_thesis: for X being set st a in X holds ( a [= "\/" (X,C) & "/\" (X,C) [= a ) let X be set ; ::_thesis: ( a in X implies ( a [= "\/" (X,C) & "/\" (X,C) [= a ) ) assume A1: a in X ; ::_thesis: ( a [= "\/" (X,C) & "/\" (X,C) [= a ) X is_less_than "\/" (X,C) by Def21; hence a [= "\/" (X,C) by A1, Def17; ::_thesis: "/\" (X,C) [= a { b where b is Element of C : b is_less_than X } is_less_than a proof let c be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( c in { b where b is Element of C : b is_less_than X } implies c [= a ) assume c in { b where b is Element of C : b is_less_than X } ; ::_thesis: c [= a then ex b being Element of C st ( c = b & b is_less_than X ) ; hence c [= a by A1, Def16; ::_thesis: verum end; hence "/\" (X,C) [= a by Def21; ::_thesis: verum end; theorem Th39: :: LATTICE3:39 for C being complete Lattice for a being Element of C for X being set st a is_less_than X holds a [= "/\" (X,C) proof let C be complete Lattice; ::_thesis: for a being Element of C for X being set st a is_less_than X holds a [= "/\" (X,C) let a be Element of C; ::_thesis: for X being set st a is_less_than X holds a [= "/\" (X,C) let X be set ; ::_thesis: ( a is_less_than X implies a [= "/\" (X,C) ) assume a is_less_than X ; ::_thesis: a [= "/\" (X,C) then a in { b where b is Element of C : b is_less_than X } ; hence a [= "/\" (X,C) by Th38; ::_thesis: verum end; theorem Th40: :: LATTICE3:40 for C being complete Lattice for a being Element of C for X being set st a in X & X is_less_than a holds "\/" (X,C) = a proof let C be complete Lattice; ::_thesis: for a being Element of C for X being set st a in X & X is_less_than a holds "\/" (X,C) = a let a be Element of C; ::_thesis: for X being set st a in X & X is_less_than a holds "\/" (X,C) = a let X be set ; ::_thesis: ( a in X & X is_less_than a implies "\/" (X,C) = a ) assume that A1: a in X and A2: X is_less_than a ; ::_thesis: "\/" (X,C) = a A3: "\/" (X,C) [= a by A2, Def21; a [= "\/" (X,C) by A1, Th38; hence "\/" (X,C) = a by A3, LATTICES:8; ::_thesis: verum end; theorem Th41: :: LATTICE3:41 for C being complete Lattice for a being Element of C for X being set st a in X & a is_less_than X holds "/\" (X,C) = a proof let C be complete Lattice; ::_thesis: for a being Element of C for X being set st a in X & a is_less_than X holds "/\" (X,C) = a let a be Element of C; ::_thesis: for X being set st a in X & a is_less_than X holds "/\" (X,C) = a let X be set ; ::_thesis: ( a in X & a is_less_than X implies "/\" (X,C) = a ) assume that A1: a in X and A2: a is_less_than X ; ::_thesis: "/\" (X,C) = a A3: "/\" (X,C) [= a by A1, Th38; a [= "/\" (X,C) by A2, Th39; hence "/\" (X,C) = a by A3, LATTICES:8; ::_thesis: verum end; theorem :: LATTICE3:42 for C being complete Lattice for a being Element of C holds ( "\/" {a} = a & "/\" {a} = a ) proof let C be complete Lattice; ::_thesis: for a being Element of C holds ( "\/" {a} = a & "/\" {a} = a ) let a be Element of C; ::_thesis: ( "\/" {a} = a & "/\" {a} = a ) A1: a in {a} by TARSKI:def_1; {a} is_less_than a proof let b be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( b in {a} implies b [= a ) assume b in {a} ; ::_thesis: b [= a hence b [= a by TARSKI:def_1; ::_thesis: verum end; hence "\/" {a} = a by A1, Th40; ::_thesis: "/\" {a} = a a is_less_than {a} proof let b be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( b in {a} implies a [= b ) assume b in {a} ; ::_thesis: a [= b hence a [= b by TARSKI:def_1; ::_thesis: verum end; hence "/\" {a} = a by A1, Th41; ::_thesis: verum end; theorem :: LATTICE3:43 for C being complete Lattice for a, b being Element of C holds ( a "\/" b = "\/" {a,b} & a "/\" b = "/\" {a,b} ) proof let C be complete Lattice; ::_thesis: for a, b being Element of C holds ( a "\/" b = "\/" {a,b} & a "/\" b = "/\" {a,b} ) let a, b be Element of C; ::_thesis: ( a "\/" b = "\/" {a,b} & a "/\" b = "/\" {a,b} ) A1: {a,b} is_less_than a "\/" b proof let c be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( c in {a,b} implies c [= a "\/" b ) assume A2: c in {a,b} ; ::_thesis: c [= a "\/" b A3: a [= a "\/" b by LATTICES:5; b [= b "\/" a by LATTICES:5; hence c [= a "\/" b by A2, A3, TARSKI:def_2; ::_thesis: verum end; A4: a in {a,b} by TARSKI:def_2; A5: b in {a,b} by TARSKI:def_2; now__::_thesis:_for_c_being_Element_of_C_st_{a,b}_is_less_than_c_holds_ a_"\/"_b_[=_c let c be Element of C; ::_thesis: ( {a,b} is_less_than c implies a "\/" b [= c ) assume A6: {a,b} is_less_than c ; ::_thesis: a "\/" b [= c then A7: a [= c by A4, Def17; b [= c by A5, A6, Def17; hence a "\/" b [= c by A7, FILTER_0:6; ::_thesis: verum end; hence a "\/" b = "\/" {a,b} by A1, Def21; ::_thesis: a "/\" b = "/\" {a,b} a "/\" b is_less_than {a,b} proof let c be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( c in {a,b} implies a "/\" b [= c ) assume c in {a,b} ; ::_thesis: a "/\" b [= c then ( c = a or ( c = b & b "/\" a = a "/\" b ) ) by TARSKI:def_2; hence a "/\" b [= c by LATTICES:6; ::_thesis: verum end; then A8: a "/\" b in { c where c is Element of C : c is_less_than {a,b} } ; { c where c is Element of C : c is_less_than {a,b} } is_less_than a "/\" b proof let d be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( d in { c where c is Element of C : c is_less_than {a,b} } implies d [= a "/\" b ) assume d in { c where c is Element of C : c is_less_than {a,b} } ; ::_thesis: d [= a "/\" b then A9: ex c being Element of C st ( d = c & c is_less_than {a,b} ) ; then A10: d [= a by A4, Def16; d [= b by A5, A9, Def16; hence d [= a "/\" b by A10, FILTER_0:7; ::_thesis: verum end; hence a "/\" b = "/\" {a,b} by A8, Th40; ::_thesis: verum end; theorem :: LATTICE3:44 for C being complete Lattice for a being Element of C holds ( a = "\/" ( { b where b is Element of C : b [= a } ,C) & a = "/\" ( { c where c is Element of C : a [= c } ,C) ) proof let C be complete Lattice; ::_thesis: for a being Element of C holds ( a = "\/" ( { b where b is Element of C : b [= a } ,C) & a = "/\" ( { c where c is Element of C : a [= c } ,C) ) let a be Element of C; ::_thesis: ( a = "\/" ( { b where b is Element of C : b [= a } ,C) & a = "/\" ( { c where c is Element of C : a [= c } ,C) ) set X = { b where b is Element of C : b [= a } ; set Y = { c where c is Element of C : a [= c } ; A1: a in { b where b is Element of C : b [= a } ; A2: a in { c where c is Element of C : a [= c } ; { b where b is Element of C : b [= a } is_less_than a proof let b be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( b in { b where b is Element of C : b [= a } implies b [= a ) assume b in { b where b is Element of C : b [= a } ; ::_thesis: b [= a then ex c being Element of C st ( b = c & c [= a ) ; hence b [= a ; ::_thesis: verum end; hence a = "\/" ( { b where b is Element of C : b [= a } ,C) by A1, Th40; ::_thesis: a = "/\" ( { c where c is Element of C : a [= c } ,C) a is_less_than { c where c is Element of C : a [= c } proof let b be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( b in { c where c is Element of C : a [= c } implies a [= b ) assume b in { c where c is Element of C : a [= c } ; ::_thesis: a [= b then ex c being Element of C st ( b = c & a [= c ) ; hence a [= b ; ::_thesis: verum end; hence a = "/\" ( { c where c is Element of C : a [= c } ,C) by A2, Th41; ::_thesis: verum end; theorem Th45: :: LATTICE3:45 for C being complete Lattice for X, Y being set st X c= Y holds ( "\/" (X,C) [= "\/" (Y,C) & "/\" (Y,C) [= "/\" (X,C) ) proof let C be complete Lattice; ::_thesis: for X, Y being set st X c= Y holds ( "\/" (X,C) [= "\/" (Y,C) & "/\" (Y,C) [= "/\" (X,C) ) let X, Y be set ; ::_thesis: ( X c= Y implies ( "\/" (X,C) [= "\/" (Y,C) & "/\" (Y,C) [= "/\" (X,C) ) ) assume A1: X c= Y ; ::_thesis: ( "\/" (X,C) [= "\/" (Y,C) & "/\" (Y,C) [= "/\" (X,C) ) X is_less_than "\/" (Y,C) proof let a be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( a in X implies a [= "\/" (Y,C) ) assume A2: a in X ; ::_thesis: a [= "\/" (Y,C) Y is_less_than "\/" (Y,C) by Def21; hence a [= "\/" (Y,C) by A1, A2, Def17; ::_thesis: verum end; hence "\/" (X,C) [= "\/" (Y,C) by Def21; ::_thesis: "/\" (Y,C) [= "/\" (X,C) "/\" (Y,C) is_less_than X proof let a be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( a in X implies "/\" (Y,C) [= a ) assume A3: a in X ; ::_thesis: "/\" (Y,C) [= a "/\" (Y,C) is_less_than Y by Th34; hence "/\" (Y,C) [= a by A1, A3, Def16; ::_thesis: verum end; hence "/\" (Y,C) [= "/\" (X,C) by Th34; ::_thesis: verum end; theorem Th46: :: LATTICE3:46 for C being complete Lattice for X being set holds ( "\/" (X,C) = "\/" ( { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ,C) & "/\" (X,C) = "/\" ( { b where b is Element of C : ex a being Element of C st ( a [= b & a in X ) } ,C) ) proof let C be complete Lattice; ::_thesis: for X being set holds ( "\/" (X,C) = "\/" ( { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ,C) & "/\" (X,C) = "/\" ( { b where b is Element of C : ex a being Element of C st ( a [= b & a in X ) } ,C) ) let X be set ; ::_thesis: ( "\/" (X,C) = "\/" ( { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ,C) & "/\" (X,C) = "/\" ( { b where b is Element of C : ex a being Element of C st ( a [= b & a in X ) } ,C) ) set Y = { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ; set Z = { a where a is Element of C : ex b being Element of C st ( b [= a & b in X ) } ; X is_less_than "\/" ( { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ,C) proof let a be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( a in X implies a [= "\/" ( { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ,C) ) assume a in X ; ::_thesis: a [= "\/" ( { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ,C) then a in { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ; hence a [= "\/" ( { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ,C) by Th38; ::_thesis: verum end; then A1: "\/" (X,C) [= "\/" ( { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ,C) by Def21; { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } is_less_than "\/" (X,C) proof let a be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( a in { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } implies a [= "\/" (X,C) ) assume a in { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ; ::_thesis: a [= "\/" (X,C) then ex b being Element of C st ( a = b & ex c being Element of C st ( b [= c & c in X ) ) ; then consider c being Element of C such that A2: a [= c and A3: c in X ; c [= "\/" (X,C) by A3, Th38; hence a [= "\/" (X,C) by A2, LATTICES:7; ::_thesis: verum end; then "\/" ( { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ,C) [= "\/" (X,C) by Def21; hence "\/" (X,C) = "\/" ( { a where a is Element of C : ex b being Element of C st ( a [= b & b in X ) } ,C) by A1, LATTICES:8; ::_thesis: "/\" (X,C) = "/\" ( { b where b is Element of C : ex a being Element of C st ( a [= b & a in X ) } ,C) X is_greater_than "/\" ( { a where a is Element of C : ex b being Element of C st ( b [= a & b in X ) } ,C) proof let a be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( a in X implies "/\" ( { a where a is Element of C : ex b being Element of C st ( b [= a & b in X ) } ,C) [= a ) assume a in X ; ::_thesis: "/\" ( { a where a is Element of C : ex b being Element of C st ( b [= a & b in X ) } ,C) [= a then a in { a where a is Element of C : ex b being Element of C st ( b [= a & b in X ) } ; hence "/\" ( { a where a is Element of C : ex b being Element of C st ( b [= a & b in X ) } ,C) [= a by Th38; ::_thesis: verum end; then A4: "/\" ( { a where a is Element of C : ex b being Element of C st ( b [= a & b in X ) } ,C) [= "/\" (X,C) by Th34; { a where a is Element of C : ex b being Element of C st ( b [= a & b in X ) } is_greater_than "/\" (X,C) proof let a be Element of C; :: according to LATTICE3:def_16 ::_thesis: ( a in { a where a is Element of C : ex b being Element of C st ( b [= a & b in X ) } implies "/\" (X,C) [= a ) assume a in { a where a is Element of C : ex b being Element of C st ( b [= a & b in X ) } ; ::_thesis: "/\" (X,C) [= a then ex b being Element of C st ( a = b & ex c being Element of C st ( c [= b & c in X ) ) ; then consider c being Element of C such that A5: c [= a and A6: c in X ; "/\" (X,C) [= c by A6, Th38; hence "/\" (X,C) [= a by A5, LATTICES:7; ::_thesis: verum end; then "/\" (X,C) [= "/\" ( { a where a is Element of C : ex b being Element of C st ( b [= a & b in X ) } ,C) by Th34; hence "/\" (X,C) = "/\" ( { b where b is Element of C : ex a being Element of C st ( a [= b & a in X ) } ,C) by A4, LATTICES:8; ::_thesis: verum end; theorem :: LATTICE3:47 for C being complete Lattice for X, Y being set st ( for a being Element of C st a in X holds ex b being Element of C st ( a [= b & b in Y ) ) holds "\/" (X,C) [= "\/" (Y,C) proof let C be complete Lattice; ::_thesis: for X, Y being set st ( for a being Element of C st a in X holds ex b being Element of C st ( a [= b & b in Y ) ) holds "\/" (X,C) [= "\/" (Y,C) let X, Y be set ; ::_thesis: ( ( for a being Element of C st a in X holds ex b being Element of C st ( a [= b & b in Y ) ) implies "\/" (X,C) [= "\/" (Y,C) ) assume A1: for a being Element of C st a in X holds ex b being Element of C st ( a [= b & b in Y ) ; ::_thesis: "\/" (X,C) [= "\/" (Y,C) X is_less_than "\/" (Y,C) proof let a be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( a in X implies a [= "\/" (Y,C) ) assume a in X ; ::_thesis: a [= "\/" (Y,C) then consider b being Element of C such that A2: a [= b and A3: b in Y by A1; b [= "\/" (Y,C) by A3, Th38; hence a [= "\/" (Y,C) by A2, LATTICES:7; ::_thesis: verum end; hence "\/" (X,C) [= "\/" (Y,C) by Def21; ::_thesis: verum end; theorem :: LATTICE3:48 for C being complete Lattice for X being set st X c= bool the carrier of C holds "\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) proof let C be complete Lattice; ::_thesis: for X being set st X c= bool the carrier of C holds "\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) let X be set ; ::_thesis: ( X c= bool the carrier of C implies "\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) ) set Z = { ("\/" Y) where Y is Subset of C : Y in X } ; { ("\/" Y) where Y is Subset of C : Y in X } is_less_than "\/" ((union X),C) proof let a be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( a in { ("\/" Y) where Y is Subset of C : Y in X } implies a [= "\/" ((union X),C) ) assume a in { ("\/" Y) where Y is Subset of C : Y in X } ; ::_thesis: a [= "\/" ((union X),C) then consider Y being Subset of C such that A1: a = "\/" Y and A2: Y in X ; Y c= union X by A2, ZFMISC_1:74; hence a [= "\/" ((union X),C) by A1, Th45; ::_thesis: verum end; then A3: "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) [= "\/" ((union X),C) by Def21; set V = { a where a is Element of C : ex b being Element of C st ( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } ; assume A4: X c= bool the carrier of C ; ::_thesis: "\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) union X c= { a where a is Element of C : ex b being Element of C st ( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union X or x in { a where a is Element of C : ex b being Element of C st ( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } ) assume x in union X ; ::_thesis: x in { a where a is Element of C : ex b being Element of C st ( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } then consider Y being set such that A5: x in Y and A6: Y in X by TARSKI:def_4; reconsider Y = Y as Subset of C by A4, A6; reconsider a = x as Element of C by A4, A5, A6; A7: a [= "\/" Y by A5, Th38; "\/" Y in { ("\/" Y) where Y is Subset of C : Y in X } by A6; hence x in { a where a is Element of C : ex b being Element of C st ( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } by A7; ::_thesis: verum end; then "\/" ((union X),C) [= "\/" ( { a where a is Element of C : ex b being Element of C st ( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } ,C) by Th45; then "\/" ((union X),C) [= "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) by Th46; hence "\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C) by A3, LATTICES:8; ::_thesis: verum end; theorem :: LATTICE3:49 for C being complete Lattice holds ( C is 0_Lattice & Bottom C = "\/" ({},C) ) proof let C be complete Lattice; ::_thesis: ( C is 0_Lattice & Bottom C = "\/" ({},C) ) A1: now__::_thesis:_for_a_being_Element_of_C_holds_ (_("\/"_({},C))_"/\"_a_=_"\/"_({},C)_&_a_"/\"_("\/"_({},C))_=_"\/"_({},C)_) let a be Element of C; ::_thesis: ( ("\/" ({},C)) "/\" a = "\/" ({},C) & a "/\" ("\/" ({},C)) = "\/" ({},C) ) {} is_less_than ("\/" ({},C)) "/\" a proof let b be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( b in {} implies b [= ("\/" ({},C)) "/\" a ) thus ( b in {} implies b [= ("\/" ({},C)) "/\" a ) ; ::_thesis: verum end; then A2: "\/" ({},C) [= ("\/" ({},C)) "/\" a by Def21; A3: ("\/" ({},C)) "/\" a [= "\/" ({},C) by LATTICES:6; hence ("\/" ({},C)) "/\" a = "\/" ({},C) by A2, LATTICES:8; ::_thesis: a "/\" ("\/" ({},C)) = "\/" ({},C) thus a "/\" ("\/" ({},C)) = "\/" ({},C) by A2, A3, LATTICES:8; ::_thesis: verum end; then C is lower-bounded by LATTICES:def_13; hence ( C is 0_Lattice & Bottom C = "\/" ({},C) ) by A1, LATTICES:def_16; ::_thesis: verum end; theorem :: LATTICE3:50 for C being complete Lattice holds ( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) ) proof let C be complete Lattice; ::_thesis: ( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) ) set j = "\/" ( the carrier of C,C); A1: now__::_thesis:_for_a_being_Element_of_C_holds_ (_("\/"_(_the_carrier_of_C,C))_"\/"_a_=_"\/"_(_the_carrier_of_C,C)_&_a_"\/"_("\/"_(_the_carrier_of_C,C))_=_"\/"_(_the_carrier_of_C,C)_) let a be Element of C; ::_thesis: ( ("\/" ( the carrier of C,C)) "\/" a = "\/" ( the carrier of C,C) & a "\/" ("\/" ( the carrier of C,C)) = "\/" ( the carrier of C,C) ) A2: "\/" ( the carrier of C,C) [= ("\/" ( the carrier of C,C)) "\/" a by LATTICES:5; A3: ("\/" ( the carrier of C,C)) "\/" a [= "\/" ( the carrier of C,C) by Th38; hence ("\/" ( the carrier of C,C)) "\/" a = "\/" ( the carrier of C,C) by A2, LATTICES:8; ::_thesis: a "\/" ("\/" ( the carrier of C,C)) = "\/" ( the carrier of C,C) thus a "\/" ("\/" ( the carrier of C,C)) = "\/" ( the carrier of C,C) by A2, A3, LATTICES:8; ::_thesis: verum end; then C is upper-bounded by LATTICES:def_14; hence ( C is 1_Lattice & Top C = "\/" ( the carrier of C,C) ) by A1, LATTICES:def_17; ::_thesis: verum end; theorem Th51: :: LATTICE3:51 for C being complete Lattice for a, b being Element of C st C is I_Lattice holds a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C) proof let C be complete Lattice; ::_thesis: for a, b being Element of C st C is I_Lattice holds a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C) let a, b be Element of C; ::_thesis: ( C is I_Lattice implies a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C) ) set X = { a9 where a9 is Element of C : a "/\" a9 [= b } ; assume A1: C is I_Lattice ; ::_thesis: a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C) then a "/\" (a => b) [= b by FILTER_0:def_7; then A2: a => b in { a9 where a9 is Element of C : a "/\" a9 [= b } ; { a9 where a9 is Element of C : a "/\" a9 [= b } is_less_than a => b proof let c be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( c in { a9 where a9 is Element of C : a "/\" a9 [= b } implies c [= a => b ) assume c in { a9 where a9 is Element of C : a "/\" a9 [= b } ; ::_thesis: c [= a => b then ex a9 being Element of C st ( c = a9 & a "/\" a9 [= b ) ; hence c [= a => b by A1, FILTER_0:def_7; ::_thesis: verum end; hence a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C) by A2, Th40; ::_thesis: verum end; theorem :: LATTICE3:52 for C being complete Lattice st C is I_Lattice holds C is \/-distributive proof let C be complete Lattice; ::_thesis: ( C is I_Lattice implies C is \/-distributive ) assume A1: C is I_Lattice ; ::_thesis: C is \/-distributive now__::_thesis:_for_X_being_set_ for_a_being_Element_of_C_holds_a_"/\"_("\/"_(X,C))_[=_"\/"_(_{__(a_"/\"_a9)_where_a9_is_Element_of_C_:_a9_in_X__}__,C) let X be set ; ::_thesis: for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) let a be Element of C; ::_thesis: a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) set Y = { (a "/\" a9) where a9 is Element of C : a9 in X } ; set b = "\/" (X,C); set c = "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C); set Z = { b9 where b9 is Element of C : a "/\" b9 [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) } ; X is_less_than a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)) proof let b9 be Element of C; :: according to LATTICE3:def_17 ::_thesis: ( b9 in X implies b9 [= a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)) ) assume b9 in X ; ::_thesis: b9 [= a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)) then a "/\" b9 in { (a "/\" a9) where a9 is Element of C : a9 in X } ; then a "/\" b9 [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) by Th38; then A2: b9 in { b9 where b9 is Element of C : a "/\" b9 [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) } ; a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)) = "\/" ( { b9 where b9 is Element of C : a "/\" b9 [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) } ,C) by A1, Th51; hence b9 [= a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)) by A2, Th38; ::_thesis: verum end; then "\/" (X,C) [= a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C)) by Def21; then A3: a "/\" ("\/" (X,C)) [= a "/\" (a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C))) by LATTICES:9; a "/\" (a => ("\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C))) [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) by A1, FILTER_0:def_7; hence a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" a9) where a9 is Element of C : a9 in X } ,C) by A3, LATTICES:7; ::_thesis: verum end; hence C is \/-distributive by Th33; ::_thesis: verum end; theorem :: LATTICE3:53 for X being set for D being complete \/-distributive Lattice for a being Element of D holds ( a "/\" ("\/" (X,D)) = "\/" ( { (a "/\" b1) where b1 is Element of D : b1 in X } ,D) & ("\/" (X,D)) "/\" a = "\/" ( { (b2 "/\" a) where b2 is Element of D : b2 in X } ,D) ) proof let X be set ; ::_thesis: for D being complete \/-distributive Lattice for a being Element of D holds ( a "/\" ("\/" (X,D)) = "\/" ( { (a "/\" b1) where b1 is Element of D : b1 in X } ,D) & ("\/" (X,D)) "/\" a = "\/" ( { (b2 "/\" a) where b2 is Element of D : b2 in X } ,D) ) let D be complete \/-distributive Lattice; ::_thesis: for a being Element of D holds ( a "/\" ("\/" (X,D)) = "\/" ( { (a "/\" b1) where b1 is Element of D : b1 in X } ,D) & ("\/" (X,D)) "/\" a = "\/" ( { (b2 "/\" a) where b2 is Element of D : b2 in X } ,D) ) let a be Element of D; ::_thesis: ( a "/\" ("\/" (X,D)) = "\/" ( { (a "/\" b1) where b1 is Element of D : b1 in X } ,D) & ("\/" (X,D)) "/\" a = "\/" ( { (b2 "/\" a) where b2 is Element of D : b2 in X } ,D) ) A1: "\/" ( { (a "/\" b) where b is Element of D : b in X } ,D) [= a "/\" ("\/" (X,D)) by Th32; A2: a "/\" ("\/" (X,D)) [= "\/" ( { (a "/\" b) where b is Element of D : b in X } ,D) by Th33; hence a "/\" ("\/" (X,D)) = "\/" ( { (a "/\" b) where b is Element of D : b in X } ,D) by A1, LATTICES:8; ::_thesis: ("\/" (X,D)) "/\" a = "\/" ( { (b2 "/\" a) where b2 is Element of D : b2 in X } ,D) deffunc H4( Element of D) -> Element of the carrier of D = $1 "/\" a; deffunc H5( Element of D) -> Element of the carrier of D = a "/\" $1; defpred S1[ set ] means $1 in X; A3: for b being Element of D holds H5(b) = H4(b) ; { H5(b) where b is Element of D : S1[b] } = { H4(c) where c is Element of D : S1[c] } from FRAENKEL:sch_5(A3); hence ("\/" (X,D)) "/\" a = "\/" ( { (b2 "/\" a) where b2 is Element of D : b2 in X } ,D) by A1, A2, LATTICES:8; ::_thesis: verum end; theorem :: LATTICE3:54 for X being set for D being complete /\-distributive Lattice for a being Element of D holds ( a "\/" ("/\" (X,D)) = "/\" ( { (a "\/" b1) where b1 is Element of D : b1 in X } ,D) & ("/\" (X,D)) "\/" a = "/\" ( { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D) ) proof let X be set ; ::_thesis: for D being complete /\-distributive Lattice for a being Element of D holds ( a "\/" ("/\" (X,D)) = "/\" ( { (a "\/" b1) where b1 is Element of D : b1 in X } ,D) & ("/\" (X,D)) "\/" a = "/\" ( { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D) ) let D be complete /\-distributive Lattice; ::_thesis: for a being Element of D holds ( a "\/" ("/\" (X,D)) = "/\" ( { (a "\/" b1) where b1 is Element of D : b1 in X } ,D) & ("/\" (X,D)) "\/" a = "/\" ( { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D) ) let a be Element of D; ::_thesis: ( a "\/" ("/\" (X,D)) = "/\" ( { (a "\/" b1) where b1 is Element of D : b1 in X } ,D) & ("/\" (X,D)) "\/" a = "/\" ( { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D) ) defpred S1[ set ] means $1 in X; A1: "/\" ( { (a "\/" b) where b is Element of D : b in X } ,D) [= a "\/" ("/\" (X,D)) by Th36; A2: a "\/" ("/\" (X,D)) [= "/\" ( { (a "\/" b) where b is Element of D : b in X } ,D) by Th35; hence a "\/" ("/\" (X,D)) = "/\" ( { (a "\/" b) where b is Element of D : b in X } ,D) by A1, LATTICES:8; ::_thesis: ("/\" (X,D)) "\/" a = "/\" ( { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D) deffunc H4( Element of D) -> Element of the carrier of D = $1 "\/" a; deffunc H5( Element of D) -> Element of the carrier of D = a "\/" $1; A3: for b being Element of D holds H5(b) = H4(b) ; { H5(b) where b is Element of D : S1[b] } = { H4(c) where c is Element of D : S1[c] } from FRAENKEL:sch_5(A3); hence ("/\" (X,D)) "\/" a = "/\" ( { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D) by A1, A2, LATTICES:8; ::_thesis: verum end; scheme :: LATTICE3:sch 1 SingleFraenkel{ F1() -> set , F2() -> non empty set , P1[ set ] } : { F1() where a is Element of F2() : P1[a] } = {F1()} provided A1: ex a being Element of F2() st P1[a] proof thus { F1() where a is Element of F2() : P1[a] } c= {F1()} :: according to XBOOLE_0:def_10 ::_thesis: {F1()} c= { F1() where a is Element of F2() : P1[a] } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F1() where a is Element of F2() : P1[a] } or x in {F1()} ) assume x in { F1() where a is Element of F2() : P1[a] } ; ::_thesis: x in {F1()} then ex a being Element of F2() st ( x = F1() & P1[a] ) ; hence x in {F1()} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {F1()} or x in { F1() where a is Element of F2() : P1[a] } ) assume x in {F1()} ; ::_thesis: x in { F1() where a is Element of F2() : P1[a] } then x = F1() by TARSKI:def_1; hence x in { F1() where a is Element of F2() : P1[a] } by A1; ::_thesis: verum end; scheme :: LATTICE3:sch 2 FuncFraenkel{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2(), F4() -> Function, P1[ set ] } : F4() .: { F3(x) where x is Element of F1() : P1[x] } = { (F4() . F3(x)) where x is Element of F1() : P1[x] } provided A1: F2() c= dom F4() proof set f = F4(); thus F4() .: { F3(x) where x is Element of F1() : P1[x] } c= { (F4() . F3(x)) where x is Element of F1() : P1[x] } :: according to XBOOLE_0:def_10 ::_thesis: { (F4() . F3(x)) where x is Element of F1() : P1[x] } c= F4() .: { F3(x) where x is Element of F1() : P1[x] } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F4() .: { F3(x) where x is Element of F1() : P1[x] } or y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ) assume y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ; ::_thesis: y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } then consider z being set such that z in dom F4() and A2: z in { F3(x) where x is Element of F1() : P1[x] } and A3: y = F4() . z by FUNCT_1:def_6; ex x being Element of F1() st ( z = F3(x) & P1[x] ) by A2; hence y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } by A3; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } or y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ) assume y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ; ::_thesis: y in F4() .: { F3(x) where x is Element of F1() : P1[x] } then consider x being Element of F1() such that A4: y = F4() . F3(x) and A5: P1[x] ; A6: F3(x) in dom F4() by A1, TARSKI:def_3; F3(x) in { F3(z) where z is Element of F1() : P1[z] } by A5; hence y in F4() .: { F3(x) where x is Element of F1() : P1[x] } by A4, A6, FUNCT_1:def_6; ::_thesis: verum end; Lm3: now__::_thesis:_for_D_being_non_empty_set_ for_f_being_Function_of_(bool_D),D_st_(_for_a_being_Element_of_D_holds_f_._{a}_=_a_)_&_(_for_X_being_Subset-Family_of_D_holds_f_._(f_.:_X)_=_f_._(union_X)_)_holds_ ex_L_being_strict_Lattice_st_ (_H1(L)_=_D_&_(_for_X_being_Subset_of_L_holds_"\/"_X_=_f_._X_)_) let D be non empty set ; ::_thesis: for f being Function of (bool D),D st ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds ex L being strict Lattice st ( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) ) let f be Function of (bool D),D; ::_thesis: ( ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) implies ex L being strict Lattice st ( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) ) ) assume that A1: for a being Element of D holds f . {a} = a and A2: for X being Subset-Family of D holds f . (f .: X) = f . (union X) ; ::_thesis: ex L being strict Lattice st ( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) ) defpred S1[ set , set ] means f . {$1,$2} = $2; consider R being Relation of D such that A3: for x, y being set holds ( [x,y] in R iff ( x in D & y in D & S1[x,y] ) ) from RELSET_1:sch_1(); A4: dom f = bool D by FUNCT_2:def_1; A5: now__::_thesis:_for_x,_y_being_Subset_of_D_holds_f_._{(f_._x),(f_._y)}_=_f_._(x_\/_y) let x, y be Subset of D; ::_thesis: f . {(f . x),(f . y)} = f . (x \/ y) thus f . {(f . x),(f . y)} = f . (f .: {x,y}) by A4, FUNCT_1:60 .= f . (union {x,y}) by A2 .= f . (x \/ y) by ZFMISC_1:75 ; ::_thesis: verum end; A6: for x, y being Element of D for X being Subset of D st y in X holds f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } proof let x, y be Element of D; ::_thesis: for X being Subset of D st y in X holds f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } let X be Subset of D; ::_thesis: ( y in X implies f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } ) assume A7: y in X ; ::_thesis: f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } set Y = { {t,x} where t is Element of D : t in X } ; A8: X \/ {x} = union { {t,x} where t is Element of D : t in X } proof thus X \/ {x} c= union { {t,x} where t is Element of D : t in X } :: according to XBOOLE_0:def_10 ::_thesis: union { {t,x} where t is Element of D : t in X } c= X \/ {x} proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in X \/ {x} or s in union { {t,x} where t is Element of D : t in X } ) assume s in X \/ {x} ; ::_thesis: s in union { {t,x} where t is Element of D : t in X } then ( ( s in X & X c= D ) or s in {x} ) by XBOOLE_0:def_3; then ( ( s in X & s is Element of D ) or s = x ) by TARSKI:def_1; then ( ( s in {s,x} & {s,x} in { {t,x} where t is Element of D : t in X } ) or ( s in {y,x} & {y,x} in { {t,x} where t is Element of D : t in X } ) ) by A7, TARSKI:def_2; hence s in union { {t,x} where t is Element of D : t in X } by TARSKI:def_4; ::_thesis: verum end; let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in union { {t,x} where t is Element of D : t in X } or s in X \/ {x} ) assume s in union { {t,x} where t is Element of D : t in X } ; ::_thesis: s in X \/ {x} then consider Z being set such that A9: s in Z and A10: Z in { {t,x} where t is Element of D : t in X } by TARSKI:def_4; consider t being Element of D such that A11: Z = {t,x} and A12: t in X by A10; ( s = t or ( s = x & x in {x} ) ) by A9, A11, TARSKI:def_1, TARSKI:def_2; hence s in X \/ {x} by A12, XBOOLE_0:def_3; ::_thesis: verum end; { {t,x} where t is Element of D : t in X } c= bool D proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { {t,x} where t is Element of D : t in X } or s in bool D ) assume s in { {t,x} where t is Element of D : t in X } ; ::_thesis: s in bool D then s c= X \/ {x} by A8, ZFMISC_1:74; then s c= D by XBOOLE_1:1; hence s in bool D ; ::_thesis: verum end; then reconsider Y = { {t,x} where t is Element of D : t in X } as Subset-Family of D ; defpred S2[ set ] means $1 in X; deffunc H4( Element of D) -> Element of bool D = {$1,x}; A13: bool D c= dom f by FUNCT_2:def_1; f .: { H4(t) where t is Element of D : S2[t] } = { (f . H4(t)) where t is Element of D : S2[t] } from LATTICE3:sch_2(A13); then f . (union Y) = f . { (f . {t,x}) where t is Element of D : t in X } by A2; hence f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } by A8; ::_thesis: verum end; A14: R is_reflexive_in D proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in D or [x,x] in R ) assume A15: x in D ; ::_thesis: [x,x] in R then x = f . {x} by A1 .= f . {x,x} by ENUMSET1:29 ; hence [x,x] in R by A3, A15; ::_thesis: verum end; A16: R is_antisymmetric_in D proof let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in D or not y in D or not [x,y] in R or not [y,x] in R or x = y ) assume that x in D and y in D and A17: [x,y] in R and A18: [y,x] in R ; ::_thesis: x = y f . {x,y} = y by A3, A17; hence x = y by A3, A18; ::_thesis: verum end; A19: R is_transitive_in D proof let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in D or not y in D or not z in D or not [x,y] in R or not [y,z] in R or [x,z] in R ) assume that A20: x in D and A21: y in D and A22: z in D and A23: [x,y] in R and A24: [y,z] in R ; ::_thesis: [x,z] in R reconsider a = x, b = y, c = z as Element of D by A20, A21, A22; A25: f . {x,y} = y by A3, A23; A26: f . {y,z} = z by A3, A24; then f . {a,c} = f . {(f . {a}),(f . {b,c})} by A1 .= f . ({a} \/ {b,c}) by A5 .= f . {a,b,c} by ENUMSET1:2 .= f . ({a,b} \/ {c}) by ENUMSET1:3 .= f . {(f . {a,b}),(f . {c})} by A5 .= c by A1, A25, A26 ; hence [x,z] in R by A3; ::_thesis: verum end; A27: dom R = D by A14, ORDERS_1:13; field R = D by A14, ORDERS_1:13; then reconsider R = R as Order of D by A14, A16, A19, A27, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_16; set A = RelStr(# D,R #); RelStr(# D,R #) is complete proof let X be set ; :: according to LATTICE3:def_12 ::_thesis: ex a being Element of RelStr(# D,R #) st ( X is_<=_than a & ( for b being Element of RelStr(# D,R #) st X is_<=_than b holds a <= b ) ) reconsider Y = X /\ D as Subset of D by XBOOLE_1:17; reconsider a = f . Y as Element of RelStr(# D,R #) ; take a ; ::_thesis: ( X is_<=_than a & ( for b being Element of RelStr(# D,R #) st X is_<=_than b holds a <= b ) ) thus X is_<=_than a ::_thesis: for b being Element of RelStr(# D,R #) st X is_<=_than b holds a <= b proof let b be Element of RelStr(# D,R #); :: according to LATTICE3:def_9 ::_thesis: ( b in X implies b <= a ) assume b in X ; ::_thesis: b <= a then b in Y by XBOOLE_0:def_4; then {b} \/ Y = Y by ZFMISC_1:40; then a = f . {(f . {b}),a} by A5 .= f . {b,a} by A1 ; hence [b,a] in the InternalRel of RelStr(# D,R #) by A3; :: according to ORDERS_2:def_5 ::_thesis: verum end; let b be Element of RelStr(# D,R #); ::_thesis: ( X is_<=_than b implies a <= b ) assume A28: X is_<=_than b ; ::_thesis: a <= b A29: f . {a,b} = f . {a,(f . {b})} by A1 .= f . (Y \/ {b}) by A5 ; now__::_thesis:_f_._{a,b}_=_b percases ( Y <> {} or Y = {} ) ; supposeA30: Y <> {} ; ::_thesis: f . {a,b} = b set s = the Element of Y; reconsider s = the Element of Y as Element of D by A30, TARSKI:def_3; deffunc H4( Element of D) -> set = f . {$1,b}; deffunc H5( Element of D) -> Element of RelStr(# D,R #) = b; defpred S2[ set ] means $1 in Y; A31: for t being Element of D st S2[t] holds H4(t) = H5(t) proof let t be Element of D; ::_thesis: ( S2[t] implies H4(t) = H5(t) ) reconsider s = t as Element of RelStr(# D,R #) ; reconsider y = b as Element of D ; assume t in Y ; ::_thesis: H4(t) = H5(t) then t in X by XBOOLE_0:def_4; then s <= b by A28, Def9; then [t,y] in R by ORDERS_2:def_5; hence H4(t) = H5(t) by A3; ::_thesis: verum end; A32: s in Y by A30; then A33: ex t being Element of D st S2[t] ; { H4(t) where t is Element of D : S2[t] } = { H5(t) where t is Element of D : S2[t] } from FRAENKEL:sch_6(A31) .= { b where t is Element of D : S2[t] } .= {b} from LATTICE3:sch_1(A33) ; hence f . {a,b} = f . {b} by A6, A29, A32 .= b by A1 ; ::_thesis: verum end; suppose Y = {} ; ::_thesis: f . {a,b} = b hence f . {a,b} = b by A1, A29; ::_thesis: verum end; end; end; hence [a,b] in the InternalRel of RelStr(# D,R #) by A3; :: according to ORDERS_2:def_5 ::_thesis: verum end; then reconsider A = RelStr(# D,R #) as non empty strict complete Poset ; take L = latt A; ::_thesis: ( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) ) A34: ( A is with_suprema & A is with_infima ) by Th12; then A35: A = LattPOSet L by Def15; hence H1(L) = D ; ::_thesis: for X being Subset of L holds "\/" X = f . X let X be Subset of L; ::_thesis: "\/" X = f . X reconsider Y = X as Subset of D by A35; reconsider a = f . Y as Element of (LattPOSet L) by A34, Def15; set p = % a; X is_<=_than a proof let b be Element of (LattPOSet L); :: according to LATTICE3:def_9 ::_thesis: ( b in X implies b <= a ) reconsider y = b as Element of D by A34, Def15; assume b in X ; ::_thesis: b <= a then A36: X = {b} \/ X by ZFMISC_1:40; f . {y,(f . Y)} = f . {(f . {y}),(f . Y)} by A1 .= a by A5, A36 ; hence [b,a] in the InternalRel of (LattPOSet L) by A3, A35; :: according to ORDERS_2:def_5 ::_thesis: verum end; then A37: X is_less_than % a by Th31; now__::_thesis:_for_q_being_Element_of_L_st_X_is_less_than_q_holds_ %_a_[=_q let q be Element of L; ::_thesis: ( X is_less_than q implies % a [= q ) reconsider y = q as Element of D by A35; reconsider b = y as Element of (LattPOSet L) ; assume X is_less_than q ; ::_thesis: % a [= q then A38: X is_<=_than q % by Th30; A39: f . {(f . Y),b} = f . {(f . Y),(f . {y})} by A1 .= f . (Y \/ {b}) by A5 ; now__::_thesis:_f_._{a,b}_=_b percases ( Y <> {} or Y = {} ) ; supposeA40: Y <> {} ; ::_thesis: f . {a,b} = b set s = the Element of Y; reconsider s = the Element of Y as Element of D by A40, TARSKI:def_3; deffunc H4( Element of D) -> set = f . {$1,b}; deffunc H5( Element of D) -> Element of (LattPOSet L) = b; defpred S2[ set ] means $1 in Y; A41: for t being Element of D st S2[t] holds H4(t) = H5(t) proof let t be Element of D; ::_thesis: ( S2[t] implies H4(t) = H5(t) ) reconsider s = t as Element of (LattPOSet L) by A34, Def15; assume t in Y ; ::_thesis: H4(t) = H5(t) then s <= b by A38, Def9; then [t,y] in R by A35, ORDERS_2:def_5; hence H4(t) = H5(t) by A3; ::_thesis: verum end; A42: s in Y by A40; then A43: ex t being Element of D st S2[t] ; { H4(t) where t is Element of D : S2[t] } = { H5(t) where t is Element of D : S2[t] } from FRAENKEL:sch_6(A41) .= { b where t is Element of D : S2[t] } .= {b} from LATTICE3:sch_1(A43) ; hence f . {a,b} = f . {b} by A6, A39, A42 .= b by A1 ; ::_thesis: verum end; suppose Y = {} ; ::_thesis: f . {a,b} = b hence f . {a,b} = b by A1, A39; ::_thesis: verum end; end; end; then [a,b] in the InternalRel of (LattPOSet L) by A3, A35; then A44: a <= b by ORDERS_2:def_5; A45: (% a) % = % a ; q % = b ; hence % a [= q by A44, A45, Th7; ::_thesis: verum end; hence "\/" X = f . X by A37, Def21; ::_thesis: verum end; theorem :: LATTICE3:55 for D being non empty set for f being Function of (bool D),D st ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds ex L being strict complete Lattice st ( the carrier of L = D & ( for X being Subset of L holds "\/" X = f . X ) ) by Lm3;