:: YELLOW_4 semantic presentation begin theorem Th1: :: YELLOW_4:1 for L being RelStr for X being set for a being Element of L st a in X & ex_sup_of X,L holds a <= "\/" (X,L) proof let L be RelStr ; ::_thesis: for X being set for a being Element of L st a in X & ex_sup_of X,L holds a <= "\/" (X,L) let X be set ; ::_thesis: for a being Element of L st a in X & ex_sup_of X,L holds a <= "\/" (X,L) let a be Element of L; ::_thesis: ( a in X & ex_sup_of X,L implies a <= "\/" (X,L) ) assume that A1: a in X and A2: ex_sup_of X,L ; ::_thesis: a <= "\/" (X,L) X is_<=_than "\/" (X,L) by A2, YELLOW_0:def_9; hence a <= "\/" (X,L) by A1, LATTICE3:def_9; ::_thesis: verum end; theorem Th2: :: YELLOW_4:2 for L being RelStr for X being set for a being Element of L st a in X & ex_inf_of X,L holds "/\" (X,L) <= a proof let L be RelStr ; ::_thesis: for X being set for a being Element of L st a in X & ex_inf_of X,L holds "/\" (X,L) <= a let X be set ; ::_thesis: for a being Element of L st a in X & ex_inf_of X,L holds "/\" (X,L) <= a let a be Element of L; ::_thesis: ( a in X & ex_inf_of X,L implies "/\" (X,L) <= a ) assume that A1: a in X and A2: ex_inf_of X,L ; ::_thesis: "/\" (X,L) <= a X is_>=_than "/\" (X,L) by A2, YELLOW_0:def_10; hence "/\" (X,L) <= a by A1, LATTICE3:def_8; ::_thesis: verum end; definition let L be RelStr ; let A, B be Subset of L; predA is_finer_than B means :Def1: :: YELLOW_4:def 1 for a being Element of L st a in A holds ex b being Element of L st ( b in B & a <= b ); predB is_coarser_than A means :Def2: :: YELLOW_4:def 2 for b being Element of L st b in B holds ex a being Element of L st ( a in A & a <= b ); end; :: deftheorem Def1 defines is_finer_than YELLOW_4:def_1_:_ for L being RelStr for A, B being Subset of L holds ( A is_finer_than B iff for a being Element of L st a in A holds ex b being Element of L st ( b in B & a <= b ) ); :: deftheorem Def2 defines is_coarser_than YELLOW_4:def_2_:_ for L being RelStr for A, B being Subset of L holds ( B is_coarser_than A iff for b being Element of L st b in B holds ex a being Element of L st ( a in A & a <= b ) ); definition let L be non empty reflexive RelStr ; let A, B be Subset of L; :: original: is_finer_than redefine predA is_finer_than B; reflexivity for A being Subset of L holds (L,b1,b1) proof let A be Subset of L; ::_thesis: (L,A,A) let a be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( a in A implies ex b being Element of L st ( b in A & a <= b ) ) assume A1: a in A ; ::_thesis: ex b being Element of L st ( b in A & a <= b ) take b = a; ::_thesis: ( b in A & a <= b ) thus ( b in A & a <= b ) by A1; ::_thesis: verum end; :: original: is_coarser_than redefine predB is_coarser_than A; reflexivity for B being Subset of L holds (L,b1,b1) proof let A be Subset of L; ::_thesis: (L,A,A) let a be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( a in A implies ex a being Element of L st ( a in A & a <= a ) ) assume A2: a in A ; ::_thesis: ex a being Element of L st ( a in A & a <= a ) take b = a; ::_thesis: ( b in A & b <= a ) thus ( b in A & b <= a ) by A2; ::_thesis: verum end; end; theorem :: YELLOW_4:3 for L being RelStr for B being Subset of L holds {} L is_finer_than B proof let L be RelStr ; ::_thesis: for B being Subset of L holds {} L is_finer_than B let B be Subset of L; ::_thesis: {} L is_finer_than B let a be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( a in {} L implies ex b being Element of L st ( b in B & a <= b ) ) assume a in {} L ; ::_thesis: ex b being Element of L st ( b in B & a <= b ) hence ex b being Element of L st ( b in B & a <= b ) ; ::_thesis: verum end; theorem :: YELLOW_4:4 for L being transitive RelStr for A, B, C being Subset of L st A is_finer_than B & B is_finer_than C holds A is_finer_than C proof let L be transitive RelStr ; ::_thesis: for A, B, C being Subset of L st A is_finer_than B & B is_finer_than C holds A is_finer_than C let A, B, C be Subset of L; ::_thesis: ( A is_finer_than B & B is_finer_than C implies A is_finer_than C ) assume that A1: A is_finer_than B and A2: B is_finer_than C ; ::_thesis: A is_finer_than C let a be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( a in A implies ex b being Element of L st ( b in C & a <= b ) ) assume a in A ; ::_thesis: ex b being Element of L st ( b in C & a <= b ) then consider b being Element of L such that A3: b in B and A4: a <= b by A1, Def1; consider c being Element of L such that A5: ( c in C & b <= c ) by A2, A3, Def1; take c ; ::_thesis: ( c in C & a <= c ) thus ( c in C & a <= c ) by A4, A5, ORDERS_2:3; ::_thesis: verum end; theorem :: YELLOW_4:5 for L being RelStr for A, B being Subset of L st B is_finer_than A & A is lower holds B c= A proof let L be RelStr ; ::_thesis: for A, B being Subset of L st B is_finer_than A & A is lower holds B c= A let A, B be Subset of L; ::_thesis: ( B is_finer_than A & A is lower implies B c= A ) assume that A1: B is_finer_than A and A2: A is lower ; ::_thesis: B c= A let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in A ) assume A3: a in B ; ::_thesis: a in A then reconsider a1 = a as Element of L ; ex b being Element of L st ( b in A & a1 <= b ) by A1, A3, Def1; hence a in A by A2, WAYBEL_0:def_19; ::_thesis: verum end; theorem :: YELLOW_4:6 for L being RelStr for A being Subset of L holds {} L is_coarser_than A proof let L be RelStr ; ::_thesis: for A being Subset of L holds {} L is_coarser_than A let A be Subset of L; ::_thesis: {} L is_coarser_than A let b be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( b in {} L implies ex a being Element of L st ( a in A & a <= b ) ) assume b in {} L ; ::_thesis: ex a being Element of L st ( a in A & a <= b ) hence ex a being Element of L st ( a in A & a <= b ) ; ::_thesis: verum end; theorem :: YELLOW_4:7 for L being transitive RelStr for A, B, C being Subset of L st C is_coarser_than B & B is_coarser_than A holds C is_coarser_than A proof let L be transitive RelStr ; ::_thesis: for A, B, C being Subset of L st C is_coarser_than B & B is_coarser_than A holds C is_coarser_than A let A, B, C be Subset of L; ::_thesis: ( C is_coarser_than B & B is_coarser_than A implies C is_coarser_than A ) assume that A1: C is_coarser_than B and A2: B is_coarser_than A ; ::_thesis: C is_coarser_than A let c be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( c in C implies ex a being Element of L st ( a in A & a <= c ) ) assume c in C ; ::_thesis: ex a being Element of L st ( a in A & a <= c ) then consider b being Element of L such that A3: b in B and A4: b <= c by A1, Def2; consider a being Element of L such that A5: ( a in A & a <= b ) by A2, A3, Def2; take a ; ::_thesis: ( a in A & a <= c ) thus ( a in A & a <= c ) by A4, A5, ORDERS_2:3; ::_thesis: verum end; theorem :: YELLOW_4:8 for L being RelStr for A, B being Subset of L st A is_coarser_than B & B is upper holds A c= B proof let L be RelStr ; ::_thesis: for A, B being Subset of L st A is_coarser_than B & B is upper holds A c= B let A, B be Subset of L; ::_thesis: ( A is_coarser_than B & B is upper implies A c= B ) assume that A1: A is_coarser_than B and A2: B is upper ; ::_thesis: A c= B let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in B ) assume A3: a in A ; ::_thesis: a in B then reconsider a1 = a as Element of L ; ex b being Element of L st ( b in B & b <= a1 ) by A1, A3, Def2; hence a in B by A2, WAYBEL_0:def_20; ::_thesis: verum end; begin definition let L be non empty RelStr ; let D1, D2 be Subset of L; funcD1 "\/" D2 -> Subset of L equals :: YELLOW_4:def 3 { (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ; coherence { (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } is Subset of L proof { (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } c= the carrier of L proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } or q in the carrier of L ) assume q in { (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ; ::_thesis: q in the carrier of L then ex a, b being Element of L st ( q = a "\/" b & a in D1 & b in D2 ) ; hence q in the carrier of L ; ::_thesis: verum end; hence { (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } is Subset of L ; ::_thesis: verum end; end; :: deftheorem defines "\/" YELLOW_4:def_3_:_ for L being non empty RelStr for D1, D2 being Subset of L holds D1 "\/" D2 = { (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ; definition let L be antisymmetric with_suprema RelStr ; let D1, D2 be Subset of L; :: original: "\/" redefine funcD1 "\/" D2 -> Subset of L; commutativity for D1, D2 being Subset of L holds D1 "\/" D2 = D2 "\/" D1 proof let D1, D2 be Subset of L; ::_thesis: D1 "\/" D2 = D2 "\/" D1 thus D1 "\/" D2 c= D2 "\/" D1 :: according to XBOOLE_0:def_10 ::_thesis: D2 "\/" D1 c= D1 "\/" D2 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 "\/" D2 or q in D2 "\/" D1 ) assume q in D1 "\/" D2 ; ::_thesis: q in D2 "\/" D1 then ex x, y being Element of L st ( q = x "\/" y & x in D1 & y in D2 ) ; hence q in D2 "\/" D1 ; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D2 "\/" D1 or q in D1 "\/" D2 ) assume q in D2 "\/" D1 ; ::_thesis: q in D1 "\/" D2 then ex x, y being Element of L st ( q = x "\/" y & x in D2 & y in D1 ) ; hence q in D1 "\/" D2 ; ::_thesis: verum end; end; theorem :: YELLOW_4:9 for L being non empty RelStr for X being Subset of L holds X "\/" ({} L) = {} proof let L be non empty RelStr ; ::_thesis: for X being Subset of L holds X "\/" ({} L) = {} let X be Subset of L; ::_thesis: X "\/" ({} L) = {} thus X "\/" ({} L) c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= X "\/" ({} L) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X "\/" ({} L) or a in {} ) assume a in X "\/" ({} L) ; ::_thesis: a in {} then ex s, t being Element of L st ( a = s "\/" t & s in X & t in {} L ) ; hence a in {} ; ::_thesis: verum end; thus {} c= X "\/" ({} L) by XBOOLE_1:2; ::_thesis: verum end; theorem :: YELLOW_4:10 for L being non empty RelStr for X, Y being Subset of L for x, y being Element of L st x in X & y in Y holds x "\/" y in X "\/" Y ; theorem :: YELLOW_4:11 for L being antisymmetric with_suprema RelStr for A being Subset of L for B being non empty Subset of L holds A is_finer_than A "\/" B proof let L be antisymmetric with_suprema RelStr ; ::_thesis: for A being Subset of L for B being non empty Subset of L holds A is_finer_than A "\/" B let A be Subset of L; ::_thesis: for B being non empty Subset of L holds A is_finer_than A "\/" B let B be non empty Subset of L; ::_thesis: A is_finer_than A "\/" B let q be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( q in A implies ex b being Element of L st ( b in A "\/" B & q <= b ) ) assume A1: q in A ; ::_thesis: ex b being Element of L st ( b in A "\/" B & q <= b ) set b = the Element of B; take q "\/" the Element of B ; ::_thesis: ( q "\/" the Element of B in A "\/" B & q <= q "\/" the Element of B ) thus q "\/" the Element of B in A "\/" B by A1; ::_thesis: q <= q "\/" the Element of B thus q <= q "\/" the Element of B by YELLOW_0:22; ::_thesis: verum end; theorem :: YELLOW_4:12 for L being antisymmetric with_suprema RelStr for A, B being Subset of L holds A "\/" B is_coarser_than A proof let L be antisymmetric with_suprema RelStr ; ::_thesis: for A, B being Subset of L holds A "\/" B is_coarser_than A let A, B be Subset of L; ::_thesis: A "\/" B is_coarser_than A let q be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( q in A "\/" B implies ex a being Element of L st ( a in A & a <= q ) ) assume q in A "\/" B ; ::_thesis: ex a being Element of L st ( a in A & a <= q ) then consider x, y being Element of L such that A1: q = x "\/" y and A2: x in A and y in B ; take x ; ::_thesis: ( x in A & x <= q ) thus x in A by A2; ::_thesis: x <= q thus x <= q by A1, YELLOW_0:22; ::_thesis: verum end; theorem :: YELLOW_4:13 for L being reflexive antisymmetric with_suprema RelStr for A being Subset of L holds A c= A "\/" A proof let L be reflexive antisymmetric with_suprema RelStr ; ::_thesis: for A being Subset of L holds A c= A "\/" A let A be Subset of L; ::_thesis: A c= A "\/" A let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A or q in A "\/" A ) assume A1: q in A ; ::_thesis: q in A "\/" A then reconsider A1 = A as non empty Subset of L ; reconsider q1 = q as Element of A1 by A1; q1 <= q1 ; then q1 = q1 "\/" q1 by YELLOW_0:24; hence q in A "\/" A ; ::_thesis: verum end; theorem :: YELLOW_4:14 for L being transitive antisymmetric with_suprema RelStr for D1, D2, D3 being Subset of L holds (D1 "\/" D2) "\/" D3 = D1 "\/" (D2 "\/" D3) proof let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for D1, D2, D3 being Subset of L holds (D1 "\/" D2) "\/" D3 = D1 "\/" (D2 "\/" D3) let D1, D2, D3 be Subset of L; ::_thesis: (D1 "\/" D2) "\/" D3 = D1 "\/" (D2 "\/" D3) thus (D1 "\/" D2) "\/" D3 c= D1 "\/" (D2 "\/" D3) :: according to XBOOLE_0:def_10 ::_thesis: D1 "\/" (D2 "\/" D3) c= (D1 "\/" D2) "\/" D3 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (D1 "\/" D2) "\/" D3 or q in D1 "\/" (D2 "\/" D3) ) assume q in (D1 "\/" D2) "\/" D3 ; ::_thesis: q in D1 "\/" (D2 "\/" D3) then consider a1, b1 being Element of L such that A1: q = a1 "\/" b1 and A2: a1 in D1 "\/" D2 and A3: b1 in D3 ; consider a11, b11 being Element of L such that A4: a1 = a11 "\/" b11 and A5: a11 in D1 and A6: b11 in D2 by A2; ( b11 "\/" b1 in D2 "\/" D3 & q = a11 "\/" (b11 "\/" b1) ) by A1, A3, A4, A6, LATTICE3:14; hence q in D1 "\/" (D2 "\/" D3) by A5; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 "\/" (D2 "\/" D3) or q in (D1 "\/" D2) "\/" D3 ) assume q in D1 "\/" (D2 "\/" D3) ; ::_thesis: q in (D1 "\/" D2) "\/" D3 then consider a1, b1 being Element of L such that A7: ( q = a1 "\/" b1 & a1 in D1 ) and A8: b1 in D2 "\/" D3 ; consider a11, b11 being Element of L such that A9: ( b1 = a11 "\/" b11 & a11 in D2 ) and A10: b11 in D3 by A8; ( a1 "\/" a11 in D1 "\/" D2 & q = (a1 "\/" a11) "\/" b11 ) by A7, A9, LATTICE3:14; hence q in (D1 "\/" D2) "\/" D3 by A10; ::_thesis: verum end; registration let L be non empty RelStr ; let D1, D2 be non empty Subset of L; clusterD1 "\/" D2 -> non empty ; coherence not D1 "\/" D2 is empty proof consider b being set such that A1: b in D2 by XBOOLE_0:def_1; reconsider b = b as Element of D2 by A1; consider a being set such that A2: a in D1 by XBOOLE_0:def_1; reconsider a = a as Element of D1 by A2; a "\/" b in { (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ; hence not D1 "\/" D2 is empty ; ::_thesis: verum end; end; registration let L be transitive antisymmetric with_suprema RelStr ; let D1, D2 be directed Subset of L; clusterD1 "\/" D2 -> directed ; coherence D1 "\/" D2 is directed proof let a, b be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not a in D1 "\/" D2 or not b in D1 "\/" D2 or ex b1 being Element of the carrier of L st ( b1 in D1 "\/" D2 & a <= b1 & b <= b1 ) ) set X = D1 "\/" D2; assume that A1: a in D1 "\/" D2 and A2: b in D1 "\/" D2 ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in D1 "\/" D2 & a <= b1 & b <= b1 ) consider x, y being Element of L such that A3: a = x "\/" y and A4: x in D1 and A5: y in D2 by A1; consider s, t being Element of L such that A6: b = s "\/" t and A7: s in D1 and A8: t in D2 by A2; consider z2 being Element of L such that A9: z2 in D2 and A10: ( y <= z2 & t <= z2 ) by A5, A8, WAYBEL_0:def_1; consider z1 being Element of L such that A11: z1 in D1 and A12: ( x <= z1 & s <= z1 ) by A4, A7, WAYBEL_0:def_1; take z = z1 "\/" z2; ::_thesis: ( z in D1 "\/" D2 & a <= z & b <= z ) thus z in D1 "\/" D2 by A11, A9; ::_thesis: ( a <= z & b <= z ) thus ( a <= z & b <= z ) by A3, A6, A12, A10, YELLOW_3:3; ::_thesis: verum end; end; registration let L be transitive antisymmetric with_suprema RelStr ; let D1, D2 be filtered Subset of L; clusterD1 "\/" D2 -> filtered ; coherence D1 "\/" D2 is filtered proof let a, b be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not a in D1 "\/" D2 or not b in D1 "\/" D2 or ex b1 being Element of the carrier of L st ( b1 in D1 "\/" D2 & b1 <= a & b1 <= b ) ) set X = D1 "\/" D2; assume that A1: a in D1 "\/" D2 and A2: b in D1 "\/" D2 ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in D1 "\/" D2 & b1 <= a & b1 <= b ) consider x, y being Element of L such that A3: a = x "\/" y and A4: x in D1 and A5: y in D2 by A1; consider s, t being Element of L such that A6: b = s "\/" t and A7: s in D1 and A8: t in D2 by A2; consider z2 being Element of L such that A9: z2 in D2 and A10: ( y >= z2 & t >= z2 ) by A5, A8, WAYBEL_0:def_2; consider z1 being Element of L such that A11: z1 in D1 and A12: ( x >= z1 & s >= z1 ) by A4, A7, WAYBEL_0:def_2; take z = z1 "\/" z2; ::_thesis: ( z in D1 "\/" D2 & z <= a & z <= b ) thus z in D1 "\/" D2 by A11, A9; ::_thesis: ( z <= a & z <= b ) thus ( z <= a & z <= b ) by A3, A6, A12, A10, YELLOW_3:3; ::_thesis: verum end; end; registration let L be with_suprema Poset; let D1, D2 be upper Subset of L; clusterD1 "\/" D2 -> upper ; coherence D1 "\/" D2 is upper proof set X = D1 "\/" D2; let a, b be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( not a in D1 "\/" D2 or not a <= b or b in D1 "\/" D2 ) assume that A1: a in D1 "\/" D2 and A2: a <= b ; ::_thesis: b in D1 "\/" D2 consider x, y being Element of L such that A3: a = x "\/" y and A4: x in D1 and A5: y in D2 by A1; A6: ex xx being Element of L st ( x <= xx & y <= xx & ( for c being Element of L st x <= c & y <= c holds xx <= c ) ) by LATTICE3:def_10; then x <= x "\/" y by LATTICE3:def_13; then x <= b by A2, A3, YELLOW_0:def_2; then A7: b in D1 by A4, WAYBEL_0:def_20; y <= x "\/" y by A6, LATTICE3:def_13; then y <= b by A2, A3, YELLOW_0:def_2; then A8: b in D2 by A5, WAYBEL_0:def_20; b <= b ; then b = b "\/" b by YELLOW_0:24; hence b in D1 "\/" D2 by A7, A8; ::_thesis: verum end; end; theorem Th15: :: YELLOW_4:15 for L being non empty RelStr for Y being Subset of L for x being Element of L holds {x} "\/" Y = { (x "\/" y) where y is Element of L : y in Y } proof let L be non empty RelStr ; ::_thesis: for Y being Subset of L for x being Element of L holds {x} "\/" Y = { (x "\/" y) where y is Element of L : y in Y } let Y be Subset of L; ::_thesis: for x being Element of L holds {x} "\/" Y = { (x "\/" y) where y is Element of L : y in Y } let x be Element of L; ::_thesis: {x} "\/" Y = { (x "\/" y) where y is Element of L : y in Y } thus {x} "\/" Y c= { (x "\/" y) where y is Element of L : y in Y } :: according to XBOOLE_0:def_10 ::_thesis: { (x "\/" y) where y is Element of L : y in Y } c= {x} "\/" Y proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "\/" Y or q in { (x "\/" y) where y is Element of L : y in Y } ) assume q in {x} "\/" Y ; ::_thesis: q in { (x "\/" y) where y is Element of L : y in Y } then consider s, t being Element of L such that A1: q = s "\/" t and A2: s in {x} and A3: t in Y ; s = x by A2, TARSKI:def_1; hence q in { (x "\/" y) where y is Element of L : y in Y } by A1, A3; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (x "\/" y) where y is Element of L : y in Y } or q in {x} "\/" Y ) assume q in { (x "\/" y) where y is Element of L : y in Y } ; ::_thesis: q in {x} "\/" Y then A4: ex y being Element of L st ( q = x "\/" y & y in Y ) ; x in {x} by TARSKI:def_1; hence q in {x} "\/" Y by A4; ::_thesis: verum end; theorem :: YELLOW_4:16 for L being non empty RelStr for A, B, C being Subset of L holds A "\/" (B \/ C) = (A "\/" B) \/ (A "\/" C) proof let L be non empty RelStr ; ::_thesis: for A, B, C being Subset of L holds A "\/" (B \/ C) = (A "\/" B) \/ (A "\/" C) let A, B, C be Subset of L; ::_thesis: A "\/" (B \/ C) = (A "\/" B) \/ (A "\/" C) thus A "\/" (B \/ C) c= (A "\/" B) \/ (A "\/" C) :: according to XBOOLE_0:def_10 ::_thesis: (A "\/" B) \/ (A "\/" C) c= A "\/" (B \/ C) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A "\/" (B \/ C) or q in (A "\/" B) \/ (A "\/" C) ) assume q in A "\/" (B \/ C) ; ::_thesis: q in (A "\/" B) \/ (A "\/" C) then consider a, y being Element of L such that A1: ( q = a "\/" y & a in A ) and A2: y in B \/ C ; ( y in B or y in C ) by A2, XBOOLE_0:def_3; then ( q in A "\/" B or q in A "\/" C ) by A1; hence q in (A "\/" B) \/ (A "\/" C) by XBOOLE_0:def_3; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (A "\/" B) \/ (A "\/" C) or q in A "\/" (B \/ C) ) assume A3: q in (A "\/" B) \/ (A "\/" C) ; ::_thesis: q in A "\/" (B \/ C) percases ( q in A "\/" B or q in A "\/" C ) by A3, XBOOLE_0:def_3; suppose q in A "\/" B ; ::_thesis: q in A "\/" (B \/ C) then consider a, b being Element of L such that A4: ( q = a "\/" b & a in A ) and A5: b in B ; b in B \/ C by A5, XBOOLE_0:def_3; hence q in A "\/" (B \/ C) by A4; ::_thesis: verum end; suppose q in A "\/" C ; ::_thesis: q in A "\/" (B \/ C) then consider a, b being Element of L such that A6: ( q = a "\/" b & a in A ) and A7: b in C ; b in B \/ C by A7, XBOOLE_0:def_3; hence q in A "\/" (B \/ C) by A6; ::_thesis: verum end; end; end; theorem :: YELLOW_4:17 for L being reflexive antisymmetric with_suprema RelStr for A, B, C being Subset of L holds A \/ (B "\/" C) c= (A \/ B) "\/" (A \/ C) proof let L be reflexive antisymmetric with_suprema RelStr ; ::_thesis: for A, B, C being Subset of L holds A \/ (B "\/" C) c= (A \/ B) "\/" (A \/ C) let A, B, C be Subset of L; ::_thesis: A \/ (B "\/" C) c= (A \/ B) "\/" (A \/ C) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A \/ (B "\/" C) or q in (A \/ B) "\/" (A \/ C) ) assume A1: q in A \/ (B "\/" C) ; ::_thesis: q in (A \/ B) "\/" (A \/ C) percases ( q in A or q in B "\/" C ) by A1, XBOOLE_0:def_3; supposeA2: q in A ; ::_thesis: q in (A \/ B) "\/" (A \/ C) then reconsider q1 = q as Element of L ; q1 <= q1 ; then A3: q1 = q1 "\/" q1 by YELLOW_0:24; ( q1 in A \/ B & q1 in A \/ C ) by A2, XBOOLE_0:def_3; hence q in (A \/ B) "\/" (A \/ C) by A3; ::_thesis: verum end; suppose q in B "\/" C ; ::_thesis: q in (A \/ B) "\/" (A \/ C) then consider b, c being Element of L such that A4: q = b "\/" c and A5: ( b in B & c in C ) ; ( b in A \/ B & c in A \/ C ) by A5, XBOOLE_0:def_3; hence q in (A \/ B) "\/" (A \/ C) by A4; ::_thesis: verum end; end; end; theorem :: YELLOW_4:18 for L being antisymmetric with_suprema RelStr for A being upper Subset of L for B, C being Subset of L holds (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C) proof let L be antisymmetric with_suprema RelStr ; ::_thesis: for A being upper Subset of L for B, C being Subset of L holds (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C) let A be upper Subset of L; ::_thesis: for B, C being Subset of L holds (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C) let B, C be Subset of L; ::_thesis: (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (A \/ B) "\/" (A \/ C) or q in A \/ (B "\/" C) ) assume q in (A \/ B) "\/" (A \/ C) ; ::_thesis: q in A \/ (B "\/" C) then consider x, y being Element of L such that A1: q = x "\/" y and A2: ( x in A \/ B & y in A \/ C ) ; A3: x <= x "\/" y by YELLOW_0:22; A4: y <= x "\/" y by YELLOW_0:22; percases ( ( x in A & y in A ) or ( x in A & y in C ) or ( x in B & y in A ) or ( x in B & y in C ) ) by A2, XBOOLE_0:def_3; suppose ( x in A & y in A ) ; ::_thesis: q in A \/ (B "\/" C) then q in A by A1, A3, WAYBEL_0:def_20; hence q in A \/ (B "\/" C) by XBOOLE_0:def_3; ::_thesis: verum end; suppose ( x in A & y in C ) ; ::_thesis: q in A \/ (B "\/" C) then q in A by A1, A3, WAYBEL_0:def_20; hence q in A \/ (B "\/" C) by XBOOLE_0:def_3; ::_thesis: verum end; suppose ( x in B & y in A ) ; ::_thesis: q in A \/ (B "\/" C) then q in A by A1, A4, WAYBEL_0:def_20; hence q in A \/ (B "\/" C) by XBOOLE_0:def_3; ::_thesis: verum end; suppose ( x in B & y in C ) ; ::_thesis: q in A \/ (B "\/" C) then x "\/" y in B "\/" C ; hence q in A \/ (B "\/" C) by A1, XBOOLE_0:def_3; ::_thesis: verum end; end; end; Lm1: now__::_thesis:_for_L_being_non_empty_RelStr_ for_x,_y_being_Element_of_L_holds__{__(a_"\/"_b)_where_a,_b_is_Element_of_L_:_(_a_in_{x}_&_b_in_{y}_)__}__=_{(x_"\/"_y)} let L be non empty RelStr ; ::_thesis: for x, y being Element of L holds { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "\/" y)} let x, y be Element of L; ::_thesis: { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "\/" y)} thus { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "\/" y)} ::_thesis: verum proof thus { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } c= {(x "\/" y)} :: according to XBOOLE_0:def_10 ::_thesis: {(x "\/" y)} c= { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } or q in {(x "\/" y)} ) assume q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } ; ::_thesis: q in {(x "\/" y)} then consider u, v being Element of L such that A1: q = u "\/" v and A2: ( u in {x} & v in {y} ) ; ( u = x & v = y ) by A2, TARSKI:def_1; hence q in {(x "\/" y)} by A1, TARSKI:def_1; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(x "\/" y)} or q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } ) assume q in {(x "\/" y)} ; ::_thesis: q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } then A3: q = x "\/" y by TARSKI:def_1; ( x in {x} & y in {y} ) by TARSKI:def_1; hence q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } by A3; ::_thesis: verum end; end; Lm2: now__::_thesis:_for_L_being_non_empty_RelStr_ for_x,_y,_z_being_Element_of_L_holds__{__(a_"\/"_b)_where_a,_b_is_Element_of_L_:_(_a_in_{x}_&_b_in_{y,z}_)__}__=_{(x_"\/"_y),(x_"\/"_z)} let L be non empty RelStr ; ::_thesis: for x, y, z being Element of L holds { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)} let x, y, z be Element of L; ::_thesis: { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)} thus { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)} ::_thesis: verum proof thus { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } c= {(x "\/" y),(x "\/" z)} :: according to XBOOLE_0:def_10 ::_thesis: {(x "\/" y),(x "\/" z)} c= { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } or q in {(x "\/" y),(x "\/" z)} ) assume q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } ; ::_thesis: q in {(x "\/" y),(x "\/" z)} then consider u, v being Element of L such that A1: q = u "\/" v and A2: u in {x} and A3: v in {y,z} ; A4: ( v = y or v = z ) by A3, TARSKI:def_2; u = x by A2, TARSKI:def_1; hence q in {(x "\/" y),(x "\/" z)} by A1, A4, TARSKI:def_2; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(x "\/" y),(x "\/" z)} or q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } ) A5: z in {y,z} by TARSKI:def_2; assume q in {(x "\/" y),(x "\/" z)} ; ::_thesis: q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } then A6: ( q = x "\/" y or q = x "\/" z ) by TARSKI:def_2; ( x in {x} & y in {y,z} ) by TARSKI:def_1, TARSKI:def_2; hence q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } by A6, A5; ::_thesis: verum end; end; theorem :: YELLOW_4:19 for L being non empty RelStr for x, y being Element of L holds {x} "\/" {y} = {(x "\/" y)} by Lm1; theorem :: YELLOW_4:20 for L being non empty RelStr for x, y, z being Element of L holds {x} "\/" {y,z} = {(x "\/" y),(x "\/" z)} by Lm2; theorem :: YELLOW_4:21 for L being non empty RelStr for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds X1 "\/" X2 c= Y1 "\/" Y2 proof let L be non empty RelStr ; ::_thesis: for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds X1 "\/" X2 c= Y1 "\/" Y2 let X1, X2, Y1, Y2 be Subset of L; ::_thesis: ( X1 c= Y1 & X2 c= Y2 implies X1 "\/" X2 c= Y1 "\/" Y2 ) assume A1: ( X1 c= Y1 & X2 c= Y2 ) ; ::_thesis: X1 "\/" X2 c= Y1 "\/" Y2 let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X1 "\/" X2 or q in Y1 "\/" Y2 ) assume q in X1 "\/" X2 ; ::_thesis: q in Y1 "\/" Y2 then ex x, y being Element of L st ( q = x "\/" y & x in X1 & y in X2 ) ; hence q in Y1 "\/" Y2 by A1; ::_thesis: verum end; theorem :: YELLOW_4:22 for L being reflexive antisymmetric with_suprema RelStr for D being Subset of L for x being Element of L st x is_<=_than D holds {x} "\/" D = D proof let L be reflexive antisymmetric with_suprema RelStr ; ::_thesis: for D being Subset of L for x being Element of L st x is_<=_than D holds {x} "\/" D = D let D be Subset of L; ::_thesis: for x being Element of L st x is_<=_than D holds {x} "\/" D = D let x be Element of L; ::_thesis: ( x is_<=_than D implies {x} "\/" D = D ) assume A1: x is_<=_than D ; ::_thesis: {x} "\/" D = D A2: {x} "\/" D = { (x "\/" y) where y is Element of L : y in D } by Th15; thus {x} "\/" D c= D :: according to XBOOLE_0:def_10 ::_thesis: D c= {x} "\/" D proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "\/" D or q in D ) assume q in {x} "\/" D ; ::_thesis: q in D then consider y being Element of L such that A3: q = x "\/" y and A4: y in D by A2; x <= y by A1, A4, LATTICE3:def_8; hence q in D by A3, A4, YELLOW_0:24; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D or q in {x} "\/" D ) assume A5: q in D ; ::_thesis: q in {x} "\/" D then reconsider D1 = D as non empty Subset of L ; reconsider y = q as Element of D1 by A5; x <= y by A1, LATTICE3:def_8; then q = x "\/" y by YELLOW_0:24; hence q in {x} "\/" D by A2; ::_thesis: verum end; theorem :: YELLOW_4:23 for L being antisymmetric with_suprema RelStr for D being Subset of L for x being Element of L holds x is_<=_than {x} "\/" D proof let L be antisymmetric with_suprema RelStr ; ::_thesis: for D being Subset of L for x being Element of L holds x is_<=_than {x} "\/" D let D be Subset of L; ::_thesis: for x being Element of L holds x is_<=_than {x} "\/" D let x be Element of L; ::_thesis: x is_<=_than {x} "\/" D let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in {x} "\/" D or x <= b ) A1: {x} "\/" D = { (x "\/" h) where h is Element of L : h in D } by Th15; assume b in {x} "\/" D ; ::_thesis: x <= b then consider h being Element of L such that A2: b = x "\/" h and h in D by A1; ex w being Element of L st ( x <= w & h <= w & ( for c being Element of L st x <= c & h <= c holds w <= c ) ) by LATTICE3:def_10; hence x <= b by A2, LATTICE3:def_13; ::_thesis: verum end; theorem :: YELLOW_4:24 for L being with_suprema Poset for X being Subset of L for x being Element of L st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds x "\/" (inf X) <= inf ({x} "\/" X) proof let L be with_suprema Poset; ::_thesis: for X being Subset of L for x being Element of L st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds x "\/" (inf X) <= inf ({x} "\/" X) let X be Subset of L; ::_thesis: for x being Element of L st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds x "\/" (inf X) <= inf ({x} "\/" X) let x be Element of L; ::_thesis: ( ex_inf_of {x} "\/" X,L & ex_inf_of X,L implies x "\/" (inf X) <= inf ({x} "\/" X) ) assume that A1: ex_inf_of {x} "\/" X,L and A2: ex_inf_of X,L ; ::_thesis: x "\/" (inf X) <= inf ({x} "\/" X) A3: {x} "\/" X = { (x "\/" y) where y is Element of L : y in X } by Th15; {x} "\/" X is_>=_than x "\/" (inf X) proof let q be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not q in {x} "\/" X or x "\/" (inf X) <= q ) assume q in {x} "\/" X ; ::_thesis: x "\/" (inf X) <= q then consider y being Element of L such that A4: q = x "\/" y and A5: y in X by A3; ( x <= x & y >= inf X ) by A2, A5, Th2; hence x "\/" (inf X) <= q by A4, YELLOW_3:3; ::_thesis: verum end; hence x "\/" (inf X) <= inf ({x} "\/" X) by A1, YELLOW_0:def_10; ::_thesis: verum end; theorem Th25: :: YELLOW_4:25 for L being non empty transitive antisymmetric complete RelStr for A being Subset of L for B being non empty Subset of L holds A is_<=_than sup (A "\/" B) proof let L be non empty transitive antisymmetric complete RelStr ; ::_thesis: for A being Subset of L for B being non empty Subset of L holds A is_<=_than sup (A "\/" B) let A be Subset of L; ::_thesis: for B being non empty Subset of L holds A is_<=_than sup (A "\/" B) let B be non empty Subset of L; ::_thesis: A is_<=_than sup (A "\/" B) set b = the Element of B; let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in A or x <= sup (A "\/" B) ) assume x in A ; ::_thesis: x <= sup (A "\/" B) then A1: x "\/" the Element of B in A "\/" B ; ex xx being Element of L st ( x <= xx & the Element of B <= xx & ( for c being Element of L st x <= c & the Element of B <= c holds xx <= c ) ) by LATTICE3:def_10; then A2: x <= x "\/" the Element of B by LATTICE3:def_13; ex_sup_of A "\/" B,L by YELLOW_0:17; then A "\/" B is_<=_than sup (A "\/" B) by YELLOW_0:def_9; then x "\/" the Element of B <= sup (A "\/" B) by A1, LATTICE3:def_9; hence x <= sup (A "\/" B) by A2, YELLOW_0:def_2; ::_thesis: verum end; theorem :: YELLOW_4:26 for L being transitive antisymmetric with_suprema RelStr for a, b being Element of L for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds a "\/" b is_<=_than A "\/" B proof let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for a, b being Element of L for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds a "\/" b is_<=_than A "\/" B let a, b be Element of L; ::_thesis: for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds a "\/" b is_<=_than A "\/" B let A, B be Subset of L; ::_thesis: ( a is_<=_than A & b is_<=_than B implies a "\/" b is_<=_than A "\/" B ) assume A1: ( a is_<=_than A & b is_<=_than B ) ; ::_thesis: a "\/" b is_<=_than A "\/" B let q be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not q in A "\/" B or a "\/" b <= q ) assume q in A "\/" B ; ::_thesis: a "\/" b <= q then consider x, y being Element of L such that A2: q = x "\/" y and A3: ( x in A & y in B ) ; ( a <= x & b <= y ) by A1, A3, LATTICE3:def_8; hence a "\/" b <= q by A2, YELLOW_3:3; ::_thesis: verum end; theorem Th27: :: YELLOW_4:27 for L being transitive antisymmetric with_suprema RelStr for a, b being Element of L for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds a "\/" b is_>=_than A "\/" B proof let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for a, b being Element of L for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds a "\/" b is_>=_than A "\/" B let a, b be Element of L; ::_thesis: for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds a "\/" b is_>=_than A "\/" B let A, B be Subset of L; ::_thesis: ( a is_>=_than A & b is_>=_than B implies a "\/" b is_>=_than A "\/" B ) assume A1: ( a is_>=_than A & b is_>=_than B ) ; ::_thesis: a "\/" b is_>=_than A "\/" B let q be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not q in A "\/" B or q <= a "\/" b ) assume q in A "\/" B ; ::_thesis: q <= a "\/" b then consider x, y being Element of L such that A2: q = x "\/" y and A3: ( x in A & y in B ) ; ( a >= x & b >= y ) by A1, A3, LATTICE3:def_9; hence q <= a "\/" b by A2, YELLOW_3:3; ::_thesis: verum end; theorem :: YELLOW_4:28 for L being non empty complete Poset for A, B being non empty Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B) proof let L be non empty complete Poset; ::_thesis: for A, B being non empty Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B) let A, B be non empty Subset of L; ::_thesis: sup (A "\/" B) = (sup A) "\/" (sup B) B is_<=_than sup (A "\/" B) by Th25; then A1: sup B <= sup (A "\/" B) by YELLOW_0:32; A is_<=_than sup (A "\/" B) by Th25; then sup A <= sup (A "\/" B) by YELLOW_0:32; then A2: (sup A) "\/" (sup B) <= (sup (A "\/" B)) "\/" (sup (A "\/" B)) by A1, YELLOW_3:3; ( A is_<=_than sup A & B is_<=_than sup B ) by YELLOW_0:32; then ( ex_sup_of A "\/" B,L & A "\/" B is_<=_than (sup A) "\/" (sup B) ) by Th27, YELLOW_0:17; then A3: sup (A "\/" B) <= (sup A) "\/" (sup B) by YELLOW_0:def_9; sup (A "\/" B) <= sup (A "\/" B) ; then (sup (A "\/" B)) "\/" (sup (A "\/" B)) = sup (A "\/" B) by YELLOW_0:24; hence sup (A "\/" B) = (sup A) "\/" (sup B) by A3, A2, ORDERS_2:2; ::_thesis: verum end; theorem Th29: :: YELLOW_4:29 for L being antisymmetric with_suprema RelStr for X being Subset of L for Y being non empty Subset of L holds X c= downarrow (X "\/" Y) proof let L be antisymmetric with_suprema RelStr ; ::_thesis: for X being Subset of L for Y being non empty Subset of L holds X c= downarrow (X "\/" Y) let X be Subset of L; ::_thesis: for Y being non empty Subset of L holds X c= downarrow (X "\/" Y) let Y be non empty Subset of L; ::_thesis: X c= downarrow (X "\/" Y) consider y being set such that A1: y in Y by XBOOLE_0:def_1; reconsider y = y as Element of Y by A1; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X or q in downarrow (X "\/" Y) ) assume A2: q in X ; ::_thesis: q in downarrow (X "\/" Y) then reconsider X1 = X as non empty Subset of L ; reconsider x = q as Element of X1 by A2; ex s being Element of L st ( x <= s & y <= s & ( for c being Element of L st x <= c & y <= c holds s <= c ) ) by LATTICE3:def_10; then A3: x <= x "\/" y by LATTICE3:def_13; ( downarrow (X "\/" Y) = { s where s is Element of L : ex y being Element of L st ( s <= y & y in X "\/" Y ) } & x "\/" y in X1 "\/" Y ) by WAYBEL_0:14; hence q in downarrow (X "\/" Y) by A3; ::_thesis: verum end; theorem :: YELLOW_4:30 for L being with_suprema Poset for x, y being Element of (InclPoset (Ids L)) for X, Y being Subset of L st x = X & y = Y holds x "\/" y = downarrow (X "\/" Y) proof let L be with_suprema Poset; ::_thesis: for x, y being Element of (InclPoset (Ids L)) for X, Y being Subset of L st x = X & y = Y holds x "\/" y = downarrow (X "\/" Y) let x, y be Element of (InclPoset (Ids L)); ::_thesis: for X, Y being Subset of L st x = X & y = Y holds x "\/" y = downarrow (X "\/" Y) let X, Y be Subset of L; ::_thesis: ( x = X & y = Y implies x "\/" y = downarrow (X "\/" Y) ) assume that A1: x = X and A2: y = Y ; ::_thesis: x "\/" y = downarrow (X "\/" Y) reconsider X1 = X, Y1 = Y as non empty directed Subset of L by A1, A2, YELLOW_2:41; reconsider d = downarrow (X1 "\/" Y1) as Element of (InclPoset (Ids L)) by YELLOW_2:41; Y c= d by Th29; then A3: y <= d by A2, YELLOW_1:3; X c= d by Th29; then x <= d by A1, YELLOW_1:3; then ( d <= d & x "\/" y <= d "\/" d ) by A3, YELLOW_3:3; then x "\/" y <= d by YELLOW_0:24; hence x "\/" y c= downarrow (X "\/" Y) by YELLOW_1:3; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (X "\/" Y) c= x "\/" y consider Z being Subset of L such that A4: Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st ( a in x & b in y & z = a "\/" b ) ) } and ex_sup_of {x,y}, InclPoset (Ids L) and A5: x "\/" y = downarrow Z by YELLOW_2:44; X "\/" Y c= Z proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X "\/" Y or q in Z ) assume q in X "\/" Y ; ::_thesis: q in Z then ex s, t being Element of L st ( q = s "\/" t & s in X & t in Y ) ; hence q in Z by A1, A2, A4; ::_thesis: verum end; hence downarrow (X "\/" Y) c= x "\/" y by A5, YELLOW_3:6; ::_thesis: verum end; theorem :: YELLOW_4:31 for L being non empty RelStr for D being Subset of [:L,L:] holds union { X where X is Subset of L : ex x being Element of L st ( X = {x} "\/" (proj2 D) & x in proj1 D ) } = (proj1 D) "\/" (proj2 D) proof let L be non empty RelStr ; ::_thesis: for D being Subset of [:L,L:] holds union { X where X is Subset of L : ex x being Element of L st ( X = {x} "\/" (proj2 D) & x in proj1 D ) } = (proj1 D) "\/" (proj2 D) let D be Subset of [:L,L:]; ::_thesis: union { X where X is Subset of L : ex x being Element of L st ( X = {x} "\/" (proj2 D) & x in proj1 D ) } = (proj1 D) "\/" (proj2 D) set D1 = proj1 D; set D2 = proj2 D; defpred S1[ set ] means ex x being Element of L st ( \$1 = {x} "\/" (proj2 D) & x in proj1 D ); thus union { X where X is Subset of L : S1[X] } c= (proj1 D) "\/" (proj2 D) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 D) "\/" (proj2 D) c= union { X where X is Subset of L : ex x being Element of L st ( X = {x} "\/" (proj2 D) & x in proj1 D ) } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in union { X where X is Subset of L : S1[X] } or q in (proj1 D) "\/" (proj2 D) ) assume q in union { X where X is Subset of L : S1[X] } ; ::_thesis: q in (proj1 D) "\/" (proj2 D) then consider w being set such that A1: q in w and A2: w in { X where X is Subset of L : S1[X] } by TARSKI:def_4; consider e being Subset of L such that A3: w = e and A4: S1[e] by A2; consider p being Element of L such that A5: e = {p} "\/" (proj2 D) and A6: p in proj1 D by A4; {p} "\/" (proj2 D) = { (p "\/" y) where y is Element of L : y in proj2 D } by Th15; then ex y being Element of L st ( q = p "\/" y & y in proj2 D ) by A1, A3, A5; hence q in (proj1 D) "\/" (proj2 D) by A6; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (proj1 D) "\/" (proj2 D) or q in union { X where X is Subset of L : ex x being Element of L st ( X = {x} "\/" (proj2 D) & x in proj1 D ) } ) assume q in (proj1 D) "\/" (proj2 D) ; ::_thesis: q in union { X where X is Subset of L : ex x being Element of L st ( X = {x} "\/" (proj2 D) & x in proj1 D ) } then consider x, y being Element of L such that A7: q = x "\/" y and A8: x in proj1 D and A9: y in proj2 D ; {x} "\/" (proj2 D) = { (x "\/" d) where d is Element of L : d in proj2 D } by Th15; then A10: q in {x} "\/" (proj2 D) by A7, A9; {x} "\/" (proj2 D) in { X where X is Subset of L : S1[X] } by A8; hence q in union { X where X is Subset of L : ex x being Element of L st ( X = {x} "\/" (proj2 D) & x in proj1 D ) } by A10, TARSKI:def_4; ::_thesis: verum end; theorem Th32: :: YELLOW_4:32 for L being transitive antisymmetric with_suprema RelStr for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2) proof let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2) let D1, D2 be Subset of L; ::_thesis: downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2) A1: downarrow ((downarrow D1) "\/" (downarrow D2)) = { x where x is Element of L : ex t being Element of L st ( x <= t & t in (downarrow D1) "\/" (downarrow D2) ) } by WAYBEL_0:14; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in downarrow ((downarrow D1) "\/" (downarrow D2)) or y in downarrow (D1 "\/" D2) ) assume y in downarrow ((downarrow D1) "\/" (downarrow D2)) ; ::_thesis: y in downarrow (D1 "\/" D2) then consider x being Element of L such that A2: y = x and A3: ex t being Element of L st ( x <= t & t in (downarrow D1) "\/" (downarrow D2) ) by A1; consider x1 being Element of L such that A4: x <= x1 and A5: x1 in (downarrow D1) "\/" (downarrow D2) by A3; consider a, b being Element of L such that A6: x1 = a "\/" b and A7: a in downarrow D1 and A8: b in downarrow D2 by A5; downarrow D2 = { s2 where s2 is Element of L : ex z being Element of L st ( s2 <= z & z in D2 ) } by WAYBEL_0:14; then consider B1 being Element of L such that A9: b = B1 and A10: ex z being Element of L st ( B1 <= z & z in D2 ) by A8; consider b1 being Element of L such that A11: B1 <= b1 and A12: b1 in D2 by A10; downarrow D1 = { s1 where s1 is Element of L : ex z being Element of L st ( s1 <= z & z in D1 ) } by WAYBEL_0:14; then consider A1 being Element of L such that A13: a = A1 and A14: ex z being Element of L st ( A1 <= z & z in D1 ) by A7; consider a1 being Element of L such that A15: A1 <= a1 and A16: a1 in D1 by A14; x1 <= a1 "\/" b1 by A6, A13, A9, A15, A11, YELLOW_3:3; then A17: ( downarrow (D1 "\/" D2) = { s where s is Element of L : ex z being Element of L st ( s <= z & z in D1 "\/" D2 ) } & x <= a1 "\/" b1 ) by A4, ORDERS_2:3, WAYBEL_0:14; a1 "\/" b1 in D1 "\/" D2 by A16, A12; hence y in downarrow (D1 "\/" D2) by A2, A17; ::_thesis: verum end; theorem :: YELLOW_4:33 for L being with_suprema Poset for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2) proof let L be with_suprema Poset; ::_thesis: for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2) let D1, D2 be Subset of L; ::_thesis: downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2) A1: downarrow (D1 "\/" D2) = { s where s is Element of L : ex z being Element of L st ( s <= z & z in D1 "\/" D2 ) } by WAYBEL_0:14; thus downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2) by Th32; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (D1 "\/" D2) c= downarrow ((downarrow D1) "\/" (downarrow D2)) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in downarrow (D1 "\/" D2) or q in downarrow ((downarrow D1) "\/" (downarrow D2)) ) assume q in downarrow (D1 "\/" D2) ; ::_thesis: q in downarrow ((downarrow D1) "\/" (downarrow D2)) then consider s being Element of L such that A2: q = s and A3: ex z being Element of L st ( s <= z & z in D1 "\/" D2 ) by A1; A4: downarrow ((downarrow D1) "\/" (downarrow D2)) = { x where x is Element of L : ex t being Element of L st ( x <= t & t in (downarrow D1) "\/" (downarrow D2) ) } by WAYBEL_0:14; A5: ( D1 is Subset of (downarrow D1) & D2 is Subset of (downarrow D2) ) by WAYBEL_0:16; consider x being Element of L such that A6: s <= x and A7: x in D1 "\/" D2 by A3; ex a, b being Element of L st ( x = a "\/" b & a in D1 & b in D2 ) by A7; then x in (downarrow D1) "\/" (downarrow D2) by A5; hence q in downarrow ((downarrow D1) "\/" (downarrow D2)) by A4, A2, A6; ::_thesis: verum end; theorem Th34: :: YELLOW_4:34 for L being transitive antisymmetric with_suprema RelStr for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2) proof let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2) let D1, D2 be Subset of L; ::_thesis: uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2) A1: uparrow ((uparrow D1) "\/" (uparrow D2)) = { x where x is Element of L : ex t being Element of L st ( x >= t & t in (uparrow D1) "\/" (uparrow D2) ) } by WAYBEL_0:15; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in uparrow ((uparrow D1) "\/" (uparrow D2)) or y in uparrow (D1 "\/" D2) ) assume y in uparrow ((uparrow D1) "\/" (uparrow D2)) ; ::_thesis: y in uparrow (D1 "\/" D2) then consider x being Element of L such that A2: y = x and A3: ex t being Element of L st ( x >= t & t in (uparrow D1) "\/" (uparrow D2) ) by A1; consider x1 being Element of L such that A4: x >= x1 and A5: x1 in (uparrow D1) "\/" (uparrow D2) by A3; consider a, b being Element of L such that A6: x1 = a "\/" b and A7: a in uparrow D1 and A8: b in uparrow D2 by A5; uparrow D2 = { s2 where s2 is Element of L : ex z being Element of L st ( s2 >= z & z in D2 ) } by WAYBEL_0:15; then consider B1 being Element of L such that A9: b = B1 and A10: ex z being Element of L st ( B1 >= z & z in D2 ) by A8; consider b1 being Element of L such that A11: B1 >= b1 and A12: b1 in D2 by A10; uparrow D1 = { s1 where s1 is Element of L : ex z being Element of L st ( s1 >= z & z in D1 ) } by WAYBEL_0:15; then consider A1 being Element of L such that A13: a = A1 and A14: ex z being Element of L st ( A1 >= z & z in D1 ) by A7; consider a1 being Element of L such that A15: A1 >= a1 and A16: a1 in D1 by A14; x1 >= a1 "\/" b1 by A6, A13, A9, A15, A11, YELLOW_3:3; then A17: ( uparrow (D1 "\/" D2) = { s where s is Element of L : ex z being Element of L st ( s >= z & z in D1 "\/" D2 ) } & x >= a1 "\/" b1 ) by A4, ORDERS_2:3, WAYBEL_0:15; a1 "\/" b1 in D1 "\/" D2 by A16, A12; hence y in uparrow (D1 "\/" D2) by A2, A17; ::_thesis: verum end; theorem :: YELLOW_4:35 for L being with_suprema Poset for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2) proof let L be with_suprema Poset; ::_thesis: for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2) let D1, D2 be Subset of L; ::_thesis: uparrow ((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2) A1: uparrow (D1 "\/" D2) = { s where s is Element of L : ex z being Element of L st ( s >= z & z in D1 "\/" D2 ) } by WAYBEL_0:15; thus uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2) by Th34; :: according to XBOOLE_0:def_10 ::_thesis: uparrow (D1 "\/" D2) c= uparrow ((uparrow D1) "\/" (uparrow D2)) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow (D1 "\/" D2) or q in uparrow ((uparrow D1) "\/" (uparrow D2)) ) assume q in uparrow (D1 "\/" D2) ; ::_thesis: q in uparrow ((uparrow D1) "\/" (uparrow D2)) then consider s being Element of L such that A2: q = s and A3: ex z being Element of L st ( s >= z & z in D1 "\/" D2 ) by A1; A4: uparrow ((uparrow D1) "\/" (uparrow D2)) = { x where x is Element of L : ex t being Element of L st ( x >= t & t in (uparrow D1) "\/" (uparrow D2) ) } by WAYBEL_0:15; A5: ( D1 is Subset of (uparrow D1) & D2 is Subset of (uparrow D2) ) by WAYBEL_0:16; consider x being Element of L such that A6: s >= x and A7: x in D1 "\/" D2 by A3; ex a, b being Element of L st ( x = a "\/" b & a in D1 & b in D2 ) by A7; then x in (uparrow D1) "\/" (uparrow D2) by A5; hence q in uparrow ((uparrow D1) "\/" (uparrow D2)) by A4, A2, A6; ::_thesis: verum end; begin definition let L be non empty RelStr ; let D1, D2 be Subset of L; funcD1 "/\" D2 -> Subset of L equals :: YELLOW_4:def 4 { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ; coherence { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } is Subset of L proof { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } c= the carrier of L proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } or q in the carrier of L ) assume q in { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ; ::_thesis: q in the carrier of L then ex a, b being Element of L st ( q = a "/\" b & a in D1 & b in D2 ) ; hence q in the carrier of L ; ::_thesis: verum end; hence { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } is Subset of L ; ::_thesis: verum end; end; :: deftheorem defines "/\" YELLOW_4:def_4_:_ for L being non empty RelStr for D1, D2 being Subset of L holds D1 "/\" D2 = { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ; definition let L be antisymmetric with_infima RelStr ; let D1, D2 be Subset of L; :: original: "/\" redefine funcD1 "/\" D2 -> Subset of L; commutativity for D1, D2 being Subset of L holds D1 "/\" D2 = D2 "/\" D1 proof let D1, D2 be Subset of L; ::_thesis: D1 "/\" D2 = D2 "/\" D1 thus D1 "/\" D2 c= D2 "/\" D1 :: according to XBOOLE_0:def_10 ::_thesis: D2 "/\" D1 c= D1 "/\" D2 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 "/\" D2 or q in D2 "/\" D1 ) assume q in D1 "/\" D2 ; ::_thesis: q in D2 "/\" D1 then ex x, y being Element of L st ( q = x "/\" y & x in D1 & y in D2 ) ; hence q in D2 "/\" D1 ; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D2 "/\" D1 or q in D1 "/\" D2 ) assume q in D2 "/\" D1 ; ::_thesis: q in D1 "/\" D2 then ex x, y being Element of L st ( q = x "/\" y & x in D2 & y in D1 ) ; hence q in D1 "/\" D2 ; ::_thesis: verum end; end; theorem :: YELLOW_4:36 for L being non empty RelStr for X being Subset of L holds X "/\" ({} L) = {} proof let L be non empty RelStr ; ::_thesis: for X being Subset of L holds X "/\" ({} L) = {} let X be Subset of L; ::_thesis: X "/\" ({} L) = {} thus X "/\" ({} L) c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= X "/\" ({} L) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X "/\" ({} L) or a in {} ) assume a in X "/\" ({} L) ; ::_thesis: a in {} then ex s, t being Element of L st ( a = s "/\" t & s in X & t in {} L ) ; hence a in {} ; ::_thesis: verum end; thus {} c= X "/\" ({} L) by XBOOLE_1:2; ::_thesis: verum end; theorem :: YELLOW_4:37 for L being non empty RelStr for X, Y being Subset of L for x, y being Element of L st x in X & y in Y holds x "/\" y in X "/\" Y ; theorem :: YELLOW_4:38 for L being antisymmetric with_infima RelStr for A being Subset of L for B being non empty Subset of L holds A is_coarser_than A "/\" B proof let L be antisymmetric with_infima RelStr ; ::_thesis: for A being Subset of L for B being non empty Subset of L holds A is_coarser_than A "/\" B let A be Subset of L; ::_thesis: for B being non empty Subset of L holds A is_coarser_than A "/\" B let B be non empty Subset of L; ::_thesis: A is_coarser_than A "/\" B consider b being set such that A1: b in B by XBOOLE_0:def_1; reconsider b = b as Element of B by A1; let q be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( q in A implies ex a being Element of L st ( a in A "/\" B & a <= q ) ) assume A2: q in A ; ::_thesis: ex a being Element of L st ( a in A "/\" B & a <= q ) take q "/\" b ; ::_thesis: ( q "/\" b in A "/\" B & q "/\" b <= q ) thus q "/\" b in A "/\" B by A2; ::_thesis: q "/\" b <= q thus q "/\" b <= q by YELLOW_0:23; ::_thesis: verum end; theorem :: YELLOW_4:39 for L being antisymmetric with_infima RelStr for A, B being Subset of L holds A "/\" B is_finer_than A proof let L be antisymmetric with_infima RelStr ; ::_thesis: for A, B being Subset of L holds A "/\" B is_finer_than A let A, B be Subset of L; ::_thesis: A "/\" B is_finer_than A let q be Element of L; :: according to YELLOW_4:def_1 ::_thesis: ( q in A "/\" B implies ex b being Element of L st ( b in A & q <= b ) ) assume q in A "/\" B ; ::_thesis: ex b being Element of L st ( b in A & q <= b ) then consider x, y being Element of L such that A1: q = x "/\" y and A2: x in A and y in B ; take x ; ::_thesis: ( x in A & q <= x ) thus x in A by A2; ::_thesis: q <= x thus q <= x by A1, YELLOW_0:23; ::_thesis: verum end; theorem :: YELLOW_4:40 for L being reflexive antisymmetric with_infima RelStr for A being Subset of L holds A c= A "/\" A proof let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for A being Subset of L holds A c= A "/\" A let A be Subset of L; ::_thesis: A c= A "/\" A let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A or q in A "/\" A ) assume A1: q in A ; ::_thesis: q in A "/\" A then reconsider A1 = A as non empty Subset of L ; reconsider q1 = q as Element of A1 by A1; q1 = q1 "/\" q1 by YELLOW_0:25; hence q in A "/\" A ; ::_thesis: verum end; theorem :: YELLOW_4:41 for L being transitive antisymmetric with_infima RelStr for D1, D2, D3 being Subset of L holds (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\" D3) proof let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for D1, D2, D3 being Subset of L holds (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\" D3) let D1, D2, D3 be Subset of L; ::_thesis: (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\" D3) thus (D1 "/\" D2) "/\" D3 c= D1 "/\" (D2 "/\" D3) :: according to XBOOLE_0:def_10 ::_thesis: D1 "/\" (D2 "/\" D3) c= (D1 "/\" D2) "/\" D3 proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (D1 "/\" D2) "/\" D3 or q in D1 "/\" (D2 "/\" D3) ) assume q in (D1 "/\" D2) "/\" D3 ; ::_thesis: q in D1 "/\" (D2 "/\" D3) then consider a1, b1 being Element of L such that A1: q = a1 "/\" b1 and A2: a1 in D1 "/\" D2 and A3: b1 in D3 ; consider a11, b11 being Element of L such that A4: a1 = a11 "/\" b11 and A5: a11 in D1 and A6: b11 in D2 by A2; ( b11 "/\" b1 in D2 "/\" D3 & q = a11 "/\" (b11 "/\" b1) ) by A1, A3, A4, A6, LATTICE3:16; hence q in D1 "/\" (D2 "/\" D3) by A5; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D1 "/\" (D2 "/\" D3) or q in (D1 "/\" D2) "/\" D3 ) assume q in D1 "/\" (D2 "/\" D3) ; ::_thesis: q in (D1 "/\" D2) "/\" D3 then consider a1, b1 being Element of L such that A7: ( q = a1 "/\" b1 & a1 in D1 ) and A8: b1 in D2 "/\" D3 ; consider a11, b11 being Element of L such that A9: ( b1 = a11 "/\" b11 & a11 in D2 ) and A10: b11 in D3 by A8; ( a1 "/\" a11 in D1 "/\" D2 & q = (a1 "/\" a11) "/\" b11 ) by A7, A9, LATTICE3:16; hence q in (D1 "/\" D2) "/\" D3 by A10; ::_thesis: verum end; registration let L be non empty RelStr ; let D1, D2 be non empty Subset of L; clusterD1 "/\" D2 -> non empty ; coherence not D1 "/\" D2 is empty proof consider b being set such that A1: b in D2 by XBOOLE_0:def_1; reconsider b = b as Element of D2 by A1; consider a being set such that A2: a in D1 by XBOOLE_0:def_1; reconsider a = a as Element of D1 by A2; a "/\" b in { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ; hence not D1 "/\" D2 is empty ; ::_thesis: verum end; end; registration let L be transitive antisymmetric with_infima RelStr ; let D1, D2 be directed Subset of L; clusterD1 "/\" D2 -> directed ; coherence D1 "/\" D2 is directed proof let a, b be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not a in D1 "/\" D2 or not b in D1 "/\" D2 or ex b1 being Element of the carrier of L st ( b1 in D1 "/\" D2 & a <= b1 & b <= b1 ) ) set X = D1 "/\" D2; assume that A1: a in D1 "/\" D2 and A2: b in D1 "/\" D2 ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in D1 "/\" D2 & a <= b1 & b <= b1 ) consider x, y being Element of L such that A3: a = x "/\" y and A4: x in D1 and A5: y in D2 by A1; consider s, t being Element of L such that A6: b = s "/\" t and A7: s in D1 and A8: t in D2 by A2; consider z2 being Element of L such that A9: z2 in D2 and A10: ( y <= z2 & t <= z2 ) by A5, A8, WAYBEL_0:def_1; consider z1 being Element of L such that A11: z1 in D1 and A12: ( x <= z1 & s <= z1 ) by A4, A7, WAYBEL_0:def_1; take z = z1 "/\" z2; ::_thesis: ( z in D1 "/\" D2 & a <= z & b <= z ) thus z in D1 "/\" D2 by A11, A9; ::_thesis: ( a <= z & b <= z ) thus ( a <= z & b <= z ) by A3, A6, A12, A10, YELLOW_3:2; ::_thesis: verum end; end; registration let L be transitive antisymmetric with_infima RelStr ; let D1, D2 be filtered Subset of L; clusterD1 "/\" D2 -> filtered ; coherence D1 "/\" D2 is filtered proof let a, b be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not a in D1 "/\" D2 or not b in D1 "/\" D2 or ex b1 being Element of the carrier of L st ( b1 in D1 "/\" D2 & b1 <= a & b1 <= b ) ) set X = D1 "/\" D2; assume that A1: a in D1 "/\" D2 and A2: b in D1 "/\" D2 ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in D1 "/\" D2 & b1 <= a & b1 <= b ) consider x, y being Element of L such that A3: a = x "/\" y and A4: x in D1 and A5: y in D2 by A1; consider s, t being Element of L such that A6: b = s "/\" t and A7: s in D1 and A8: t in D2 by A2; consider z2 being Element of L such that A9: z2 in D2 and A10: ( y >= z2 & t >= z2 ) by A5, A8, WAYBEL_0:def_2; consider z1 being Element of L such that A11: z1 in D1 and A12: ( x >= z1 & s >= z1 ) by A4, A7, WAYBEL_0:def_2; take z = z1 "/\" z2; ::_thesis: ( z in D1 "/\" D2 & z <= a & z <= b ) thus z in D1 "/\" D2 by A11, A9; ::_thesis: ( z <= a & z <= b ) thus ( z <= a & z <= b ) by A3, A6, A12, A10, YELLOW_3:2; ::_thesis: verum end; end; registration let L be Semilattice; let D1, D2 be lower Subset of L; clusterD1 "/\" D2 -> lower ; coherence D1 "/\" D2 is lower proof set X = D1 "/\" D2; let a, b be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( not a in D1 "/\" D2 or not b <= a or b in D1 "/\" D2 ) assume that A1: a in D1 "/\" D2 and A2: b <= a ; ::_thesis: b in D1 "/\" D2 consider x, y being Element of L such that A3: a = x "/\" y and A4: x in D1 and A5: y in D2 by A1; A6: ex xx being Element of L st ( x >= xx & y >= xx & ( for c being Element of L st x >= c & y >= c holds xx >= c ) ) by LATTICE3:def_11; then x "/\" y <= x by LATTICE3:def_14; then b <= x by A2, A3, YELLOW_0:def_2; then A7: b in D1 by A4, WAYBEL_0:def_19; x "/\" y <= y by A6, LATTICE3:def_14; then b <= y by A2, A3, YELLOW_0:def_2; then A8: b in D2 by A5, WAYBEL_0:def_19; b = b "/\" b by YELLOW_0:25; hence b in D1 "/\" D2 by A7, A8; ::_thesis: verum end; end; theorem Th42: :: YELLOW_4:42 for L being non empty RelStr for Y being Subset of L for x being Element of L holds {x} "/\" Y = { (x "/\" y) where y is Element of L : y in Y } proof let L be non empty RelStr ; ::_thesis: for Y being Subset of L for x being Element of L holds {x} "/\" Y = { (x "/\" y) where y is Element of L : y in Y } let Y be Subset of L; ::_thesis: for x being Element of L holds {x} "/\" Y = { (x "/\" y) where y is Element of L : y in Y } let x be Element of L; ::_thesis: {x} "/\" Y = { (x "/\" y) where y is Element of L : y in Y } thus {x} "/\" Y c= { (x "/\" y) where y is Element of L : y in Y } :: according to XBOOLE_0:def_10 ::_thesis: { (x "/\" y) where y is Element of L : y in Y } c= {x} "/\" Y proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "/\" Y or q in { (x "/\" y) where y is Element of L : y in Y } ) assume q in {x} "/\" Y ; ::_thesis: q in { (x "/\" y) where y is Element of L : y in Y } then consider s, t being Element of L such that A1: q = s "/\" t and A2: s in {x} and A3: t in Y ; s = x by A2, TARSKI:def_1; hence q in { (x "/\" y) where y is Element of L : y in Y } by A1, A3; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (x "/\" y) where y is Element of L : y in Y } or q in {x} "/\" Y ) assume q in { (x "/\" y) where y is Element of L : y in Y } ; ::_thesis: q in {x} "/\" Y then A4: ex y being Element of L st ( q = x "/\" y & y in Y ) ; x in {x} by TARSKI:def_1; hence q in {x} "/\" Y by A4; ::_thesis: verum end; theorem :: YELLOW_4:43 for L being non empty RelStr for A, B, C being Subset of L holds A "/\" (B \/ C) = (A "/\" B) \/ (A "/\" C) proof let L be non empty RelStr ; ::_thesis: for A, B, C being Subset of L holds A "/\" (B \/ C) = (A "/\" B) \/ (A "/\" C) let A, B, C be Subset of L; ::_thesis: A "/\" (B \/ C) = (A "/\" B) \/ (A "/\" C) thus A "/\" (B \/ C) c= (A "/\" B) \/ (A "/\" C) :: according to XBOOLE_0:def_10 ::_thesis: (A "/\" B) \/ (A "/\" C) c= A "/\" (B \/ C) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A "/\" (B \/ C) or q in (A "/\" B) \/ (A "/\" C) ) assume q in A "/\" (B \/ C) ; ::_thesis: q in (A "/\" B) \/ (A "/\" C) then consider a, y being Element of L such that A1: ( q = a "/\" y & a in A ) and A2: y in B \/ C ; ( y in B or y in C ) by A2, XBOOLE_0:def_3; then ( q in A "/\" B or q in A "/\" C ) by A1; hence q in (A "/\" B) \/ (A "/\" C) by XBOOLE_0:def_3; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (A "/\" B) \/ (A "/\" C) or q in A "/\" (B \/ C) ) assume A3: q in (A "/\" B) \/ (A "/\" C) ; ::_thesis: q in A "/\" (B \/ C) percases ( q in A "/\" B or q in A "/\" C ) by A3, XBOOLE_0:def_3; suppose q in A "/\" B ; ::_thesis: q in A "/\" (B \/ C) then consider a, b being Element of L such that A4: ( q = a "/\" b & a in A ) and A5: b in B ; b in B \/ C by A5, XBOOLE_0:def_3; hence q in A "/\" (B \/ C) by A4; ::_thesis: verum end; suppose q in A "/\" C ; ::_thesis: q in A "/\" (B \/ C) then consider a, b being Element of L such that A6: ( q = a "/\" b & a in A ) and A7: b in C ; b in B \/ C by A7, XBOOLE_0:def_3; hence q in A "/\" (B \/ C) by A6; ::_thesis: verum end; end; end; theorem :: YELLOW_4:44 for L being reflexive antisymmetric with_infima RelStr for A, B, C being Subset of L holds A \/ (B "/\" C) c= (A \/ B) "/\" (A \/ C) proof let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for A, B, C being Subset of L holds A \/ (B "/\" C) c= (A \/ B) "/\" (A \/ C) let A, B, C be Subset of L; ::_thesis: A \/ (B "/\" C) c= (A \/ B) "/\" (A \/ C) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A \/ (B "/\" C) or q in (A \/ B) "/\" (A \/ C) ) assume A1: q in A \/ (B "/\" C) ; ::_thesis: q in (A \/ B) "/\" (A \/ C) percases ( q in A or q in B "/\" C ) by A1, XBOOLE_0:def_3; supposeA2: q in A ; ::_thesis: q in (A \/ B) "/\" (A \/ C) then reconsider q1 = q as Element of L ; A3: q1 = q1 "/\" q1 by YELLOW_0:25; ( q1 in A \/ B & q1 in A \/ C ) by A2, XBOOLE_0:def_3; hence q in (A \/ B) "/\" (A \/ C) by A3; ::_thesis: verum end; suppose q in B "/\" C ; ::_thesis: q in (A \/ B) "/\" (A \/ C) then consider b, c being Element of L such that A4: q = b "/\" c and A5: ( b in B & c in C ) ; ( b in A \/ B & c in A \/ C ) by A5, XBOOLE_0:def_3; hence q in (A \/ B) "/\" (A \/ C) by A4; ::_thesis: verum end; end; end; theorem :: YELLOW_4:45 for L being antisymmetric with_infima RelStr for A being lower Subset of L for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C) proof let L be antisymmetric with_infima RelStr ; ::_thesis: for A being lower Subset of L for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C) let A be lower Subset of L; ::_thesis: for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C) let B, C be Subset of L; ::_thesis: (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (A \/ B) "/\" (A \/ C) or q in A \/ (B "/\" C) ) assume q in (A \/ B) "/\" (A \/ C) ; ::_thesis: q in A \/ (B "/\" C) then consider x, y being Element of L such that A1: q = x "/\" y and A2: ( x in A \/ B & y in A \/ C ) ; A3: x "/\" y <= x by YELLOW_0:23; A4: x "/\" y <= y by YELLOW_0:23; percases ( ( x in A & y in A ) or ( x in A & y in C ) or ( x in B & y in A ) or ( x in B & y in C ) ) by A2, XBOOLE_0:def_3; suppose ( x in A & y in A ) ; ::_thesis: q in A \/ (B "/\" C) then q in A by A1, A3, WAYBEL_0:def_19; hence q in A \/ (B "/\" C) by XBOOLE_0:def_3; ::_thesis: verum end; suppose ( x in A & y in C ) ; ::_thesis: q in A \/ (B "/\" C) then q in A by A1, A3, WAYBEL_0:def_19; hence q in A \/ (B "/\" C) by XBOOLE_0:def_3; ::_thesis: verum end; suppose ( x in B & y in A ) ; ::_thesis: q in A \/ (B "/\" C) then q in A by A1, A4, WAYBEL_0:def_19; hence q in A \/ (B "/\" C) by XBOOLE_0:def_3; ::_thesis: verum end; suppose ( x in B & y in C ) ; ::_thesis: q in A \/ (B "/\" C) then x "/\" y in B "/\" C ; hence q in A \/ (B "/\" C) by A1, XBOOLE_0:def_3; ::_thesis: verum end; end; end; Lm3: now__::_thesis:_for_L_being_non_empty_RelStr_ for_x,_y_being_Element_of_L_holds__{__(a_"/\"_b)_where_a,_b_is_Element_of_L_:_(_a_in_{x}_&_b_in_{y}_)__}__=_{(x_"/\"_y)} let L be non empty RelStr ; ::_thesis: for x, y being Element of L holds { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "/\" y)} let x, y be Element of L; ::_thesis: { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "/\" y)} thus { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "/\" y)} ::_thesis: verum proof thus { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } c= {(x "/\" y)} :: according to XBOOLE_0:def_10 ::_thesis: {(x "/\" y)} c= { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } or q in {(x "/\" y)} ) assume q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } ; ::_thesis: q in {(x "/\" y)} then consider u, v being Element of L such that A1: q = u "/\" v and A2: ( u in {x} & v in {y} ) ; ( u = x & v = y ) by A2, TARSKI:def_1; hence q in {(x "/\" y)} by A1, TARSKI:def_1; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(x "/\" y)} or q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } ) assume q in {(x "/\" y)} ; ::_thesis: q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } then A3: q = x "/\" y by TARSKI:def_1; ( x in {x} & y in {y} ) by TARSKI:def_1; hence q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } by A3; ::_thesis: verum end; end; Lm4: now__::_thesis:_for_L_being_non_empty_RelStr_ for_x,_y,_z_being_Element_of_L_holds__{__(a_"/\"_b)_where_a,_b_is_Element_of_L_:_(_a_in_{x}_&_b_in_{y,z}_)__}__=_{(x_"/\"_y),(x_"/\"_z)} let L be non empty RelStr ; ::_thesis: for x, y, z being Element of L holds { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)} let x, y, z be Element of L; ::_thesis: { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)} thus { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)} ::_thesis: verum proof thus { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } c= {(x "/\" y),(x "/\" z)} :: according to XBOOLE_0:def_10 ::_thesis: {(x "/\" y),(x "/\" z)} c= { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } or q in {(x "/\" y),(x "/\" z)} ) assume q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } ; ::_thesis: q in {(x "/\" y),(x "/\" z)} then consider u, v being Element of L such that A1: q = u "/\" v and A2: u in {x} and A3: v in {y,z} ; A4: ( v = y or v = z ) by A3, TARSKI:def_2; u = x by A2, TARSKI:def_1; hence q in {(x "/\" y),(x "/\" z)} by A1, A4, TARSKI:def_2; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {(x "/\" y),(x "/\" z)} or q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } ) A5: z in {y,z} by TARSKI:def_2; assume q in {(x "/\" y),(x "/\" z)} ; ::_thesis: q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } then A6: ( q = x "/\" y or q = x "/\" z ) by TARSKI:def_2; ( x in {x} & y in {y,z} ) by TARSKI:def_1, TARSKI:def_2; hence q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } by A6, A5; ::_thesis: verum end; end; theorem :: YELLOW_4:46 for L being non empty RelStr for x, y being Element of L holds {x} "/\" {y} = {(x "/\" y)} by Lm3; theorem :: YELLOW_4:47 for L being non empty RelStr for x, y, z being Element of L holds {x} "/\" {y,z} = {(x "/\" y),(x "/\" z)} by Lm4; theorem :: YELLOW_4:48 for L being non empty RelStr for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds X1 "/\" X2 c= Y1 "/\" Y2 proof let L be non empty RelStr ; ::_thesis: for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds X1 "/\" X2 c= Y1 "/\" Y2 let X1, X2, Y1, Y2 be Subset of L; ::_thesis: ( X1 c= Y1 & X2 c= Y2 implies X1 "/\" X2 c= Y1 "/\" Y2 ) assume A1: ( X1 c= Y1 & X2 c= Y2 ) ; ::_thesis: X1 "/\" X2 c= Y1 "/\" Y2 let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X1 "/\" X2 or q in Y1 "/\" Y2 ) assume q in X1 "/\" X2 ; ::_thesis: q in Y1 "/\" Y2 then ex x, y being Element of L st ( q = x "/\" y & x in X1 & y in X2 ) ; hence q in Y1 "/\" Y2 by A1; ::_thesis: verum end; theorem Th49: :: YELLOW_4:49 for L being reflexive antisymmetric with_infima RelStr for A, B being Subset of L holds A /\ B c= A "/\" B proof let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for A, B being Subset of L holds A /\ B c= A "/\" B let A, B be Subset of L; ::_thesis: A /\ B c= A "/\" B let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A /\ B or q in A "/\" B ) assume A1: q in A /\ B ; ::_thesis: q in A "/\" B then reconsider A1 = A as non empty Subset of L ; reconsider q1 = q as Element of A1 by A1, XBOOLE_0:def_4; A2: q1 = q1 "/\" q1 by YELLOW_0:25; q in B by A1, XBOOLE_0:def_4; hence q in A "/\" B by A2; ::_thesis: verum end; theorem Th50: :: YELLOW_4:50 for L being reflexive antisymmetric with_infima RelStr for A, B being lower Subset of L holds A "/\" B = A /\ B proof let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for A, B being lower Subset of L holds A "/\" B = A /\ B let A, B be lower Subset of L; ::_thesis: A "/\" B = A /\ B thus A "/\" B c= A /\ B :: according to XBOOLE_0:def_10 ::_thesis: A /\ B c= A "/\" B proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in A "/\" B or q in A /\ B ) assume q in A "/\" B ; ::_thesis: q in A /\ B then consider x, y being Element of L such that A1: q = x "/\" y and A2: x in A and A3: y in B ; A4: ex z being Element of L st ( x >= z & y >= z & ( for c being Element of L st x >= c & y >= c holds z >= c ) ) by LATTICE3:def_11; then x "/\" y <= y by LATTICE3:def_14; then A5: q in B by A1, A3, WAYBEL_0:def_19; x "/\" y <= x by A4, LATTICE3:def_14; then q in A by A1, A2, WAYBEL_0:def_19; hence q in A /\ B by A5, XBOOLE_0:def_4; ::_thesis: verum end; thus A /\ B c= A "/\" B by Th49; ::_thesis: verum end; theorem :: YELLOW_4:51 for L being reflexive antisymmetric with_infima RelStr for D being Subset of L for x being Element of L st x is_>=_than D holds {x} "/\" D = D proof let L be reflexive antisymmetric with_infima RelStr ; ::_thesis: for D being Subset of L for x being Element of L st x is_>=_than D holds {x} "/\" D = D let D be Subset of L; ::_thesis: for x being Element of L st x is_>=_than D holds {x} "/\" D = D let x be Element of L; ::_thesis: ( x is_>=_than D implies {x} "/\" D = D ) assume A1: x is_>=_than D ; ::_thesis: {x} "/\" D = D A2: {x} "/\" D = { (x "/\" y) where y is Element of L : y in D } by Th42; thus {x} "/\" D c= D :: according to XBOOLE_0:def_10 ::_thesis: D c= {x} "/\" D proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} "/\" D or q in D ) assume q in {x} "/\" D ; ::_thesis: q in D then consider y being Element of L such that A3: q = x "/\" y and A4: y in D by A2; x >= y by A1, A4, LATTICE3:def_9; hence q in D by A3, A4, YELLOW_0:25; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D or q in {x} "/\" D ) assume A5: q in D ; ::_thesis: q in {x} "/\" D then reconsider D1 = D as non empty Subset of L ; reconsider y = q as Element of D1 by A5; x >= y by A1, LATTICE3:def_9; then q = x "/\" y by YELLOW_0:25; hence q in {x} "/\" D by A2; ::_thesis: verum end; theorem :: YELLOW_4:52 for L being antisymmetric with_infima RelStr for D being Subset of L for x being Element of L holds {x} "/\" D is_<=_than x proof let L be antisymmetric with_infima RelStr ; ::_thesis: for D being Subset of L for x being Element of L holds {x} "/\" D is_<=_than x let D be Subset of L; ::_thesis: for x being Element of L holds {x} "/\" D is_<=_than x let x be Element of L; ::_thesis: {x} "/\" D is_<=_than x let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in {x} "/\" D or b <= x ) A1: {x} "/\" D = { (x "/\" h) where h is Element of L : h in D } by Th42; assume b in {x} "/\" D ; ::_thesis: b <= x then consider h being Element of L such that A2: b = x "/\" h and h in D by A1; ex w being Element of L st ( x >= w & h >= w & ( for c being Element of L st x >= c & h >= c holds w >= c ) ) by LATTICE3:def_11; hence b <= x by A2, LATTICE3:def_14; ::_thesis: verum end; theorem :: YELLOW_4:53 for L being Semilattice for X being Subset of L for x being Element of L st ex_sup_of {x} "/\" X,L & ex_sup_of X,L holds sup ({x} "/\" X) <= x "/\" (sup X) proof let L be Semilattice; ::_thesis: for X being Subset of L for x being Element of L st ex_sup_of {x} "/\" X,L & ex_sup_of X,L holds sup ({x} "/\" X) <= x "/\" (sup X) let X be Subset of L; ::_thesis: for x being Element of L st ex_sup_of {x} "/\" X,L & ex_sup_of X,L holds sup ({x} "/\" X) <= x "/\" (sup X) let x be Element of L; ::_thesis: ( ex_sup_of {x} "/\" X,L & ex_sup_of X,L implies sup ({x} "/\" X) <= x "/\" (sup X) ) assume that A1: ex_sup_of {x} "/\" X,L and A2: ex_sup_of X,L ; ::_thesis: sup ({x} "/\" X) <= x "/\" (sup X) A3: {x} "/\" X = { (x "/\" y) where y is Element of L : y in X } by Th42; {x} "/\" X is_<=_than x "/\" (sup X) proof let q be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not q in {x} "/\" X or q <= x "/\" (sup X) ) assume q in {x} "/\" X ; ::_thesis: q <= x "/\" (sup X) then consider y being Element of L such that A4: q = x "/\" y and A5: y in X by A3; ( x <= x & y <= sup X ) by A2, A5, Th1; hence q <= x "/\" (sup X) by A4, YELLOW_3:2; ::_thesis: verum end; hence sup ({x} "/\" X) <= x "/\" (sup X) by A1, YELLOW_0:def_9; ::_thesis: verum end; theorem Th54: :: YELLOW_4:54 for L being non empty transitive antisymmetric complete RelStr for A being Subset of L for B being non empty Subset of L holds A is_>=_than inf (A "/\" B) proof let L be non empty transitive antisymmetric complete RelStr ; ::_thesis: for A being Subset of L for B being non empty Subset of L holds A is_>=_than inf (A "/\" B) let A be Subset of L; ::_thesis: for B being non empty Subset of L holds A is_>=_than inf (A "/\" B) let B be non empty Subset of L; ::_thesis: A is_>=_than inf (A "/\" B) set b = the Element of B; let x be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not x in A or inf (A "/\" B) <= x ) assume x in A ; ::_thesis: inf (A "/\" B) <= x then A1: x "/\" the Element of B in A "/\" B ; ex xx being Element of L st ( x >= xx & the Element of B >= xx & ( for c being Element of L st x >= c & the Element of B >= c holds xx >= c ) ) by LATTICE3:def_11; then A2: x >= x "/\" the Element of B by LATTICE3:def_14; ex_inf_of A "/\" B,L by YELLOW_0:17; then A "/\" B is_>=_than inf (A "/\" B) by YELLOW_0:def_10; then x "/\" the Element of B >= inf (A "/\" B) by A1, LATTICE3:def_8; hence inf (A "/\" B) <= x by A2, YELLOW_0:def_2; ::_thesis: verum end; theorem Th55: :: YELLOW_4:55 for L being transitive antisymmetric with_infima RelStr for a, b being Element of L for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds a "/\" b is_<=_than A "/\" B proof let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for a, b being Element of L for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds a "/\" b is_<=_than A "/\" B let a, b be Element of L; ::_thesis: for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds a "/\" b is_<=_than A "/\" B let A, B be Subset of L; ::_thesis: ( a is_<=_than A & b is_<=_than B implies a "/\" b is_<=_than A "/\" B ) assume A1: ( a is_<=_than A & b is_<=_than B ) ; ::_thesis: a "/\" b is_<=_than A "/\" B let q be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not q in A "/\" B or a "/\" b <= q ) assume q in A "/\" B ; ::_thesis: a "/\" b <= q then consider x, y being Element of L such that A2: q = x "/\" y and A3: ( x in A & y in B ) ; ( a <= x & b <= y ) by A1, A3, LATTICE3:def_8; hence a "/\" b <= q by A2, YELLOW_3:2; ::_thesis: verum end; theorem :: YELLOW_4:56 for L being transitive antisymmetric with_infima RelStr for a, b being Element of L for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds a "/\" b is_>=_than A "/\" B proof let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for a, b being Element of L for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds a "/\" b is_>=_than A "/\" B let a, b be Element of L; ::_thesis: for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds a "/\" b is_>=_than A "/\" B let A, B be Subset of L; ::_thesis: ( a is_>=_than A & b is_>=_than B implies a "/\" b is_>=_than A "/\" B ) assume A1: ( a is_>=_than A & b is_>=_than B ) ; ::_thesis: a "/\" b is_>=_than A "/\" B let q be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not q in A "/\" B or q <= a "/\" b ) assume q in A "/\" B ; ::_thesis: q <= a "/\" b then consider x, y being Element of L such that A2: q = x "/\" y and A3: ( x in A & y in B ) ; ( a >= x & b >= y ) by A1, A3, LATTICE3:def_9; hence q <= a "/\" b by A2, YELLOW_3:2; ::_thesis: verum end; theorem :: YELLOW_4:57 for L being non empty complete Poset for A, B being non empty Subset of L holds inf (A "/\" B) = (inf A) "/\" (inf B) proof let L be non empty complete Poset; ::_thesis: for A, B being non empty Subset of L holds inf (A "/\" B) = (inf A) "/\" (inf B) let A, B be non empty Subset of L; ::_thesis: inf (A "/\" B) = (inf A) "/\" (inf B) B is_>=_than inf (A "/\" B) by Th54; then A1: inf B >= inf (A "/\" B) by YELLOW_0:33; A is_>=_than inf (A "/\" B) by Th54; then inf A >= inf (A "/\" B) by YELLOW_0:33; then A2: (inf A) "/\" (inf B) >= (inf (A "/\" B)) "/\" (inf (A "/\" B)) by A1, YELLOW_3:2; ( A is_>=_than inf A & B is_>=_than inf B ) by YELLOW_0:33; then ( ex_inf_of A "/\" B,L & A "/\" B is_>=_than (inf A) "/\" (inf B) ) by Th55, YELLOW_0:17; then A3: inf (A "/\" B) >= (inf A) "/\" (inf B) by YELLOW_0:def_10; (inf (A "/\" B)) "/\" (inf (A "/\" B)) = inf (A "/\" B) by YELLOW_0:25; hence inf (A "/\" B) = (inf A) "/\" (inf B) by A3, A2, ORDERS_2:2; ::_thesis: verum end; theorem :: YELLOW_4:58 for L being Semilattice for x, y being Element of (InclPoset (Ids L)) for x1, y1 being Subset of L st x = x1 & y = y1 holds x "/\" y = x1 "/\" y1 proof let L be Semilattice; ::_thesis: for x, y being Element of (InclPoset (Ids L)) for x1, y1 being Subset of L st x = x1 & y = y1 holds x "/\" y = x1 "/\" y1 let x, y be Element of (InclPoset (Ids L)); ::_thesis: for x1, y1 being Subset of L st x = x1 & y = y1 holds x "/\" y = x1 "/\" y1 let x1, y1 be Subset of L; ::_thesis: ( x = x1 & y = y1 implies x "/\" y = x1 "/\" y1 ) assume A1: ( x = x1 & y = y1 ) ; ::_thesis: x "/\" y = x1 "/\" y1 then A2: ( x1 is lower & y1 is lower ) by YELLOW_2:41; thus x "/\" y = x /\ y by YELLOW_2:43 .= x1 "/\" y1 by A1, A2, Th50 ; ::_thesis: verum end; theorem :: YELLOW_4:59 for L being antisymmetric with_infima RelStr for X being Subset of L for Y being non empty Subset of L holds X c= uparrow (X "/\" Y) proof let L be antisymmetric with_infima RelStr ; ::_thesis: for X being Subset of L for Y being non empty Subset of L holds X c= uparrow (X "/\" Y) let X be Subset of L; ::_thesis: for Y being non empty Subset of L holds X c= uparrow (X "/\" Y) let Y be non empty Subset of L; ::_thesis: X c= uparrow (X "/\" Y) consider y being set such that A1: y in Y by XBOOLE_0:def_1; reconsider y = y as Element of Y by A1; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in X or q in uparrow (X "/\" Y) ) assume A2: q in X ; ::_thesis: q in uparrow (X "/\" Y) then reconsider X1 = X as non empty Subset of L ; reconsider x = q as Element of X1 by A2; ex s being Element of L st ( x >= s & y >= s & ( for c being Element of L st x >= c & y >= c holds s >= c ) ) by LATTICE3:def_11; then A3: x "/\" y <= x by LATTICE3:def_14; ( uparrow (X "/\" Y) = { s where s is Element of L : ex y being Element of L st ( s >= y & y in X "/\" Y ) } & x "/\" y in X1 "/\" Y ) by WAYBEL_0:15; hence q in uparrow (X "/\" Y) by A3; ::_thesis: verum end; theorem :: YELLOW_4:60 for L being non empty RelStr for D being Subset of [:L,L:] holds union { X where X is Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D) proof let L be non empty RelStr ; ::_thesis: for D being Subset of [:L,L:] holds union { X where X is Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D) let D be Subset of [:L,L:]; ::_thesis: union { X where X is Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D) set D1 = proj1 D; set D2 = proj2 D; defpred S1[ set ] means ex x being Element of L st ( \$1 = {x} "/\" (proj2 D) & x in proj1 D ); thus union { X where X is Subset of L : S1[X] } c= (proj1 D) "/\" (proj2 D) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 D) "/\" (proj2 D) c= union { X where X is Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in union { X where X is Subset of L : S1[X] } or q in (proj1 D) "/\" (proj2 D) ) assume q in union { X where X is Subset of L : S1[X] } ; ::_thesis: q in (proj1 D) "/\" (proj2 D) then consider w being set such that A1: q in w and A2: w in { X where X is Subset of L : S1[X] } by TARSKI:def_4; consider e being Subset of L such that A3: w = e and A4: S1[e] by A2; consider p being Element of L such that A5: e = {p} "/\" (proj2 D) and A6: p in proj1 D by A4; {p} "/\" (proj2 D) = { (p "/\" y) where y is Element of L : y in proj2 D } by Th42; then ex y being Element of L st ( q = p "/\" y & y in proj2 D ) by A1, A3, A5; hence q in (proj1 D) "/\" (proj2 D) by A6; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in (proj1 D) "/\" (proj2 D) or q in union { X where X is Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } ) assume q in (proj1 D) "/\" (proj2 D) ; ::_thesis: q in union { X where X is Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } then consider x, y being Element of L such that A7: q = x "/\" y and A8: x in proj1 D and A9: y in proj2 D ; {x} "/\" (proj2 D) = { (x "/\" d) where d is Element of L : d in proj2 D } by Th42; then A10: q in {x} "/\" (proj2 D) by A7, A9; {x} "/\" (proj2 D) in { X where X is Subset of L : S1[X] } by A8; hence q in union { X where X is Subset of L : ex x being Element of L st ( X = {x} "/\" (proj2 D) & x in proj1 D ) } by A10, TARSKI:def_4; ::_thesis: verum end; theorem Th61: :: YELLOW_4:61 for L being transitive antisymmetric with_infima RelStr for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2) proof let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2) let D1, D2 be Subset of L; ::_thesis: downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2) A1: downarrow ((downarrow D1) "/\" (downarrow D2)) = { x where x is Element of L : ex t being Element of L st ( x <= t & t in (downarrow D1) "/\" (downarrow D2) ) } by WAYBEL_0:14; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in downarrow ((downarrow D1) "/\" (downarrow D2)) or y in downarrow (D1 "/\" D2) ) assume y in downarrow ((downarrow D1) "/\" (downarrow D2)) ; ::_thesis: y in downarrow (D1 "/\" D2) then consider x being Element of L such that A2: y = x and A3: ex t being Element of L st ( x <= t & t in (downarrow D1) "/\" (downarrow D2) ) by A1; consider x1 being Element of L such that A4: x <= x1 and A5: x1 in (downarrow D1) "/\" (downarrow D2) by A3; consider a, b being Element of L such that A6: x1 = a "/\" b and A7: a in downarrow D1 and A8: b in downarrow D2 by A5; downarrow D2 = { s2 where s2 is Element of L : ex z being Element of L st ( s2 <= z & z in D2 ) } by WAYBEL_0:14; then consider B1 being Element of L such that A9: b = B1 and A10: ex z being Element of L st ( B1 <= z & z in D2 ) by A8; consider b1 being Element of L such that A11: B1 <= b1 and A12: b1 in D2 by A10; downarrow D1 = { s1 where s1 is Element of L : ex z being Element of L st ( s1 <= z & z in D1 ) } by WAYBEL_0:14; then consider A1 being Element of L such that A13: a = A1 and A14: ex z being Element of L st ( A1 <= z & z in D1 ) by A7; consider a1 being Element of L such that A15: A1 <= a1 and A16: a1 in D1 by A14; x1 <= a1 "/\" b1 by A6, A13, A9, A15, A11, YELLOW_3:2; then A17: ( downarrow (D1 "/\" D2) = { s where s is Element of L : ex z being Element of L st ( s <= z & z in D1 "/\" D2 ) } & x <= a1 "/\" b1 ) by A4, ORDERS_2:3, WAYBEL_0:14; a1 "/\" b1 in D1 "/\" D2 by A16, A12; hence y in downarrow (D1 "/\" D2) by A2, A17; ::_thesis: verum end; theorem :: YELLOW_4:62 for L being Semilattice for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) = downarrow (D1 "/\" D2) proof let L be Semilattice; ::_thesis: for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) = downarrow (D1 "/\" D2) let D1, D2 be Subset of L; ::_thesis: downarrow ((downarrow D1) "/\" (downarrow D2)) = downarrow (D1 "/\" D2) A1: downarrow (D1 "/\" D2) = { s where s is Element of L : ex z being Element of L st ( s <= z & z in D1 "/\" D2 ) } by WAYBEL_0:14; thus downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2) by Th61; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (D1 "/\" D2) c= downarrow ((downarrow D1) "/\" (downarrow D2)) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in downarrow (D1 "/\" D2) or q in downarrow ((downarrow D1) "/\" (downarrow D2)) ) assume q in downarrow (D1 "/\" D2) ; ::_thesis: q in downarrow ((downarrow D1) "/\" (downarrow D2)) then consider s being Element of L such that A2: q = s and A3: ex z being Element of L st ( s <= z & z in D1 "/\" D2 ) by A1; A4: downarrow ((downarrow D1) "/\" (downarrow D2)) = { x where x is Element of L : ex t being Element of L st ( x <= t & t in (downarrow D1) "/\" (downarrow D2) ) } by WAYBEL_0:14; A5: ( D1 is Subset of (downarrow D1) & D2 is Subset of (downarrow D2) ) by WAYBEL_0:16; consider x being Element of L such that A6: s <= x and A7: x in D1 "/\" D2 by A3; ex a, b being Element of L st ( x = a "/\" b & a in D1 & b in D2 ) by A7; then x in (downarrow D1) "/\" (downarrow D2) by A5; hence q in downarrow ((downarrow D1) "/\" (downarrow D2)) by A4, A2, A6; ::_thesis: verum end; theorem Th63: :: YELLOW_4:63 for L being transitive antisymmetric with_infima RelStr for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2) proof let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2) let D1, D2 be Subset of L; ::_thesis: uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2) A1: uparrow ((uparrow D1) "/\" (uparrow D2)) = { x where x is Element of L : ex t being Element of L st ( x >= t & t in (uparrow D1) "/\" (uparrow D2) ) } by WAYBEL_0:15; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in uparrow ((uparrow D1) "/\" (uparrow D2)) or y in uparrow (D1 "/\" D2) ) assume y in uparrow ((uparrow D1) "/\" (uparrow D2)) ; ::_thesis: y in uparrow (D1 "/\" D2) then consider x being Element of L such that A2: y = x and A3: ex t being Element of L st ( x >= t & t in (uparrow D1) "/\" (uparrow D2) ) by A1; consider x1 being Element of L such that A4: x >= x1 and A5: x1 in (uparrow D1) "/\" (uparrow D2) by A3; consider a, b being Element of L such that A6: x1 = a "/\" b and A7: a in uparrow D1 and A8: b in uparrow D2 by A5; uparrow D2 = { s2 where s2 is Element of L : ex z being Element of L st ( s2 >= z & z in D2 ) } by WAYBEL_0:15; then consider B1 being Element of L such that A9: b = B1 and A10: ex z being Element of L st ( B1 >= z & z in D2 ) by A8; consider b1 being Element of L such that A11: B1 >= b1 and A12: b1 in D2 by A10; uparrow D1 = { s1 where s1 is Element of L : ex z being Element of L st ( s1 >= z & z in D1 ) } by WAYBEL_0:15; then consider A1 being Element of L such that A13: a = A1 and A14: ex z being Element of L st ( A1 >= z & z in D1 ) by A7; consider a1 being Element of L such that A15: A1 >= a1 and A16: a1 in D1 by A14; x1 >= a1 "/\" b1 by A6, A13, A9, A15, A11, YELLOW_3:2; then A17: ( uparrow (D1 "/\" D2) = { s where s is Element of L : ex z being Element of L st ( s >= z & z in D1 "/\" D2 ) } & x >= a1 "/\" b1 ) by A4, ORDERS_2:3, WAYBEL_0:15; a1 "/\" b1 in D1 "/\" D2 by A16, A12; hence y in uparrow (D1 "/\" D2) by A2, A17; ::_thesis: verum end; theorem :: YELLOW_4:64 for L being Semilattice for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) = uparrow (D1 "/\" D2) proof let L be Semilattice; ::_thesis: for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) = uparrow (D1 "/\" D2) let D1, D2 be Subset of L; ::_thesis: uparrow ((uparrow D1) "/\" (uparrow D2)) = uparrow (D1 "/\" D2) A1: uparrow (D1 "/\" D2) = { s where s is Element of L : ex z being Element of L st ( s >= z & z in D1 "/\" D2 ) } by WAYBEL_0:15; thus uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2) by Th63; :: according to XBOOLE_0:def_10 ::_thesis: uparrow (D1 "/\" D2) c= uparrow ((uparrow D1) "/\" (uparrow D2)) let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow (D1 "/\" D2) or q in uparrow ((uparrow D1) "/\" (uparrow D2)) ) assume q in uparrow (D1 "/\" D2) ; ::_thesis: q in uparrow ((uparrow D1) "/\" (uparrow D2)) then consider s being Element of L such that A2: q = s and A3: ex z being Element of L st ( s >= z & z in D1 "/\" D2 ) by A1; A4: uparrow ((uparrow D1) "/\" (uparrow D2)) = { x where x is Element of L : ex t being Element of L st ( x >= t & t in (uparrow D1) "/\" (uparrow D2) ) } by WAYBEL_0:15; A5: ( D1 is Subset of (uparrow D1) & D2 is Subset of (uparrow D2) ) by WAYBEL_0:16; consider x being Element of L such that A6: s >= x and A7: x in D1 "/\" D2 by A3; ex a, b being Element of L st ( x = a "/\" b & a in D1 & b in D2 ) by A7; then x in (uparrow D1) "/\" (uparrow D2) by A5; hence q in uparrow ((uparrow D1) "/\" (uparrow D2)) by A4, A2, A6; ::_thesis: verum end;