:: FILTER_0 semantic presentation begin theorem Th1: :: FILTER_0:1 for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr for p, q, r being Element of L st p [= q holds r "\/" p [= r "\/" q proof let L be non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr ; ::_thesis: for p, q, r being Element of L st p [= q holds r "\/" p [= r "\/" q let p, q, r be Element of L; ::_thesis: ( p [= q implies r "\/" p [= r "\/" q ) assume A1: p "\/" q = q ; :: according to LATTICES:def_3 ::_thesis: r "\/" p [= r "\/" q thus (r "\/" p) "\/" (r "\/" q) = (r "\/" (r "\/" p)) "\/" q by LATTICES:def_5 .= ((r "\/" r) "\/" p) "\/" q by LATTICES:def_5 .= (r "\/" p) "\/" q .= r "\/" q by A1, LATTICES:def_5 ; :: according to LATTICES:def_3 ::_thesis: verum end; theorem :: FILTER_0:2 for L being Lattice for p, r, q being Element of L st p [= r holds p "/\" q [= r proof let L be Lattice; ::_thesis: for p, r, q being Element of L st p [= r holds p "/\" q [= r let p, r, q be Element of L; ::_thesis: ( p [= r implies p "/\" q [= r ) assume p [= r ; ::_thesis: p "/\" q [= r then A1: p "/\" q [= r "/\" q by LATTICES:9; r "/\" q [= r by LATTICES:6; hence p "/\" q [= r by A1, LATTICES:7; ::_thesis: verum end; theorem :: FILTER_0:3 for L being Lattice for p, r, q being Element of L st p [= r holds p [= q "\/" r proof let L be Lattice; ::_thesis: for p, r, q being Element of L st p [= r holds p [= q "\/" r let p, r, q be Element of L; ::_thesis: ( p [= r implies p [= q "\/" r ) assume p [= r ; ::_thesis: p [= q "\/" r then A1: p "\/" q [= r "\/" q by Th1; p [= p "\/" q by LATTICES:5; hence p [= q "\/" r by A1, LATTICES:7; ::_thesis: verum end; theorem Th4: :: FILTER_0:4 for L being non empty join-commutative join-associative join-absorbing LattStr for a, b, c, d being Element of L st a [= b & c [= d holds a "\/" c [= b "\/" d proof let L be non empty join-commutative join-associative join-absorbing LattStr ; ::_thesis: for a, b, c, d being Element of L st a [= b & c [= d holds a "\/" c [= b "\/" d let a, b, c, d be Element of L; ::_thesis: ( a [= b & c [= d implies a "\/" c [= b "\/" d ) assume a [= b ; ::_thesis: ( not c [= d or a "\/" c [= b "\/" d ) then A1: b = a "\/" b by LATTICES:def_3; assume c [= d ; ::_thesis: a "\/" c [= b "\/" d then b "\/" d = (a "\/" b) "\/" (c "\/" d) by A1, LATTICES:def_3 .= ((b "\/" a) "\/" c) "\/" d by LATTICES:def_5 .= (b "\/" (a "\/" c)) "\/" d by LATTICES:def_5 .= (a "\/" c) "\/" (b "\/" d) by LATTICES:def_5 ; hence a "\/" c [= b "\/" d by LATTICES:def_3; ::_thesis: verum end; theorem Th5: :: FILTER_0:5 for L being non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr for a, b, c, d being Element of L st a [= b & c [= d holds a "/\" c [= b "/\" d proof let L be non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr ; ::_thesis: for a, b, c, d being Element of L st a [= b & c [= d holds a "/\" c [= b "/\" d let a, b, c, d be Element of L; ::_thesis: ( a [= b & c [= d implies a "/\" c [= b "/\" d ) assume a [= b ; ::_thesis: ( not c [= d or a "/\" c [= b "/\" d ) then A1: a "/\" b = a by LATTICES:4; assume c [= d ; ::_thesis: a "/\" c [= b "/\" d then a "/\" c = (a "/\" b) "/\" (c "/\" d) by A1, LATTICES:4 .= ((a "/\" b) "/\" c) "/\" d by LATTICES:def_7 .= (b "/\" (a "/\" c)) "/\" d by LATTICES:def_7 .= (a "/\" c) "/\" (b "/\" d) by LATTICES:def_7 ; hence a "/\" c [= b "/\" d by LATTICES:4; ::_thesis: verum end; theorem Th6: :: FILTER_0:6 for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr for a, b, c being Element of L st a [= c & b [= c holds a "\/" b [= c proof let L be non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr ; ::_thesis: for a, b, c being Element of L st a [= c & b [= c holds a "\/" b [= c let a, b, c be Element of L; ::_thesis: ( a [= c & b [= c implies a "\/" b [= c ) c "\/" c = c ; hence ( a [= c & b [= c implies a "\/" b [= c ) by Th4; ::_thesis: verum end; theorem Th7: :: FILTER_0:7 for L being non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr for a, b, c being Element of L st a [= b & a [= c holds a [= b "/\" c proof let L be non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr ; ::_thesis: for a, b, c being Element of L st a [= b & a [= c holds a [= b "/\" c let a, b, c be Element of L; ::_thesis: ( a [= b & a [= c implies a [= b "/\" c ) a "/\" a = a ; hence ( a [= b & a [= c implies a [= b "/\" c ) by Th5; ::_thesis: verum end; definition let L be Lattice; mode Filter of L is non empty final meet-closed Subset of L; end; theorem Th8: :: FILTER_0:8 for L being Lattice for S being non empty Subset of L holds ( S is Filter of L iff for p, q being Element of L holds ( ( p in S & q in S ) iff p "/\" q in S ) ) proof let L be Lattice; ::_thesis: for S being non empty Subset of L holds ( S is Filter of L iff for p, q being Element of L holds ( ( p in S & q in S ) iff p "/\" q in S ) ) let S be non empty Subset of L; ::_thesis: ( S is Filter of L iff for p, q being Element of L holds ( ( p in S & q in S ) iff p "/\" q in S ) ) thus ( S is Filter of L implies for p, q being Element of L holds ( ( p in S & q in S ) iff p "/\" q in S ) ) ::_thesis: ( ( for p, q being Element of L holds ( ( p in S & q in S ) iff p "/\" q in S ) ) implies S is Filter of L ) proof assume A1: S is Filter of L ; ::_thesis: for p, q being Element of L holds ( ( p in S & q in S ) iff p "/\" q in S ) let p, q be Element of L; ::_thesis: ( ( p in S & q in S ) iff p "/\" q in S ) thus ( p in S & q in S implies p "/\" q in S ) by A1, LATTICES:def_24; ::_thesis: ( p "/\" q in S implies ( p in S & q in S ) ) assume A2: p "/\" q in S ; ::_thesis: ( p in S & q in S ) ( p "/\" q [= p & p "/\" q [= q ) by LATTICES:6; hence ( p in S & q in S ) by A1, A2, LATTICES:def_23; ::_thesis: verum end; assume A3: for p, q being Element of L holds ( ( p in S & q in S ) iff p "/\" q in S ) ; ::_thesis: S is Filter of L S is final proof let p, q be Element of L; :: according to LATTICES:def_23 ::_thesis: ( not p [= q or not p in S or q in S ) assume that A4: p [= q and A5: p in S ; ::_thesis: q in S p "/\" q = p by A4, LATTICES:4; hence q in S by A3, A5; ::_thesis: verum end; hence S is Filter of L by A3, LATTICES:def_24; ::_thesis: verum end; theorem Th9: :: FILTER_0:9 for L being Lattice for D being non empty Subset of L holds ( D is Filter of L iff ( ( for p, q being Element of L st p in D & q in D holds p "/\" q in D ) & ( for p, q being Element of L st p in D & p [= q holds q in D ) ) ) proof let L be Lattice; ::_thesis: for D being non empty Subset of L holds ( D is Filter of L iff ( ( for p, q being Element of L st p in D & q in D holds p "/\" q in D ) & ( for p, q being Element of L st p in D & p [= q holds q in D ) ) ) let D be non empty Subset of L; ::_thesis: ( D is Filter of L iff ( ( for p, q being Element of L st p in D & q in D holds p "/\" q in D ) & ( for p, q being Element of L st p in D & p [= q holds q in D ) ) ) thus ( D is Filter of L implies ( ( for p, q being Element of L st p in D & q in D holds p "/\" q in D ) & ( for p, q being Element of L st p in D & p [= q holds q in D ) ) ) by LATTICES:def_23, LATTICES:def_24; ::_thesis: ( ( for p, q being Element of L st p in D & q in D holds p "/\" q in D ) & ( for p, q being Element of L st p in D & p [= q holds q in D ) implies D is Filter of L ) assume A1: ( ( for p, q being Element of L st p in D & q in D holds p "/\" q in D ) & ( for p, q being Element of L st p in D & p [= q holds q in D ) ) ; ::_thesis: D is Filter of L then for p, q being Element of L st p [= q & p in D holds q in D ; hence D is Filter of L by A1, LATTICES:def_23, LATTICES:def_24; ::_thesis: verum end; theorem Th10: :: FILTER_0:10 for L being Lattice for p, q being Element of L for H being Filter of L st p in H holds ( p "\/" q in H & q "\/" p in H ) proof let L be Lattice; ::_thesis: for p, q being Element of L for H being Filter of L st p in H holds ( p "\/" q in H & q "\/" p in H ) let p, q be Element of L; ::_thesis: for H being Filter of L st p in H holds ( p "\/" q in H & q "\/" p in H ) let H be Filter of L; ::_thesis: ( p in H implies ( p "\/" q in H & q "\/" p in H ) ) p [= p "\/" q by LATTICES:5; hence ( p in H implies ( p "\/" q in H & q "\/" p in H ) ) by Th9; ::_thesis: verum end; theorem Th11: :: FILTER_0:11 for L being Lattice for H being Filter of L st L is 1_Lattice holds Top L in H proof let L be Lattice; ::_thesis: for H being Filter of L st L is 1_Lattice holds Top L in H let H be Filter of L; ::_thesis: ( L is 1_Lattice implies Top L in H ) assume L is 1_Lattice ; ::_thesis: Top L in H then reconsider L = L as 1_Lattice ; consider p being Element of L such that A1: p in H by SUBSET_1:4; p [= Top L by LATTICES:19; hence Top L in H by A1, Th9; ::_thesis: verum end; theorem :: FILTER_0:12 for L being Lattice st L is 1_Lattice holds {(Top L)} is Filter of L proof let L be Lattice; ::_thesis: ( L is 1_Lattice implies {(Top L)} is Filter of L ) assume L is 1_Lattice ; ::_thesis: {(Top L)} is Filter of L then reconsider K = L as 1_Lattice ; now__::_thesis:_for_p,_q_being_Element_of_K_holds_ (_(_p_in_{(Top_K)}_&_q_in_{(Top_K)}_implies_p_"/\"_q_in_{(Top_K)}_)_&_(_p_"/\"_q_in_{(Top_K)}_implies_(_p_in_{(Top_K)}_&_q_in_{(Top_K)}_)_)_) let p, q be Element of K; ::_thesis: ( ( p in {(Top K)} & q in {(Top K)} implies p "/\" q in {(Top K)} ) & ( p "/\" q in {(Top K)} implies ( p in {(Top K)} & q in {(Top K)} ) ) ) A1: ( p [= Top K & q [= Top K ) by LATTICES:19; A2: ( p in {(Top K)} iff p = Top K ) by TARSKI:def_1; hence ( p in {(Top K)} & q in {(Top K)} implies p "/\" q in {(Top K)} ) by LATTICES:17; ::_thesis: ( p "/\" q in {(Top K)} implies ( p in {(Top K)} & q in {(Top K)} ) ) assume p "/\" q in {(Top K)} ; ::_thesis: ( p in {(Top K)} & q in {(Top K)} ) then A3: p "/\" q = Top K by TARSKI:def_1; ( p "/\" q [= p & q "/\" p [= q ) by LATTICES:6; hence ( p in {(Top K)} & q in {(Top K)} ) by A2, A3, A1, LATTICES:8; ::_thesis: verum end; hence {(Top L)} is Filter of L by Th8; ::_thesis: verum end; theorem :: FILTER_0:13 for L being Lattice for p being Element of L st {p} is Filter of L holds L is upper-bounded proof let L be Lattice; ::_thesis: for p being Element of L st {p} is Filter of L holds L is upper-bounded let p be Element of L; ::_thesis: ( {p} is Filter of L implies L is upper-bounded ) assume {p} is Filter of L ; ::_thesis: L is upper-bounded then reconsider F = {p} as Filter of L ; take p ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of L holds ( p "\/" b1 = p & b1 "\/" p = p ) let q be Element of L; ::_thesis: ( p "\/" q = p & q "\/" p = p ) p in F by TARSKI:def_1; then p "\/" q in F by Th10; hence ( p "\/" q = p & q "\/" p = p ) by TARSKI:def_1; ::_thesis: verum end; theorem Th14: :: FILTER_0:14 for L being Lattice holds the carrier of L is Filter of L proof let L be Lattice; ::_thesis: the carrier of L is Filter of L the carrier of L = [#] L ; hence the carrier of L is Filter of L ; ::_thesis: verum end; definition let L be Lattice; func<.L.) -> Filter of L equals :: FILTER_0:def 1 the carrier of L; coherence the carrier of L is Filter of L by Th14; end; :: deftheorem defines <. FILTER_0:def_1_:_ for L being Lattice holds <.L.) = the carrier of L; definition let L be Lattice; let p be Element of L; func<.p.) -> Filter of L equals :: FILTER_0:def 2 { q where q is Element of L : p [= q } ; coherence { q where q is Element of L : p [= q } is Filter of L proof set D = { q where q is Element of L : p [= q } ; p in { q where q is Element of L : p [= q } ; then reconsider F = { q where q is Element of L : p [= q } as non empty set ; F c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in the carrier of L ) assume x in F ; ::_thesis: x in the carrier of L then ex q being Element of L st ( x = q & p [= q ) ; hence x in the carrier of L ; ::_thesis: verum end; then reconsider F = F as non empty Subset of L ; A1: now__::_thesis:_for_r,_q_being_Element_of_L_st_r_in_F_&_q_in_F_holds_ r_"/\"_q_in_F let r, q be Element of L; ::_thesis: ( r in F & q in F implies r "/\" q in F ) assume r in F ; ::_thesis: ( q in F implies r "/\" q in F ) then ex r1 being Element of L st ( r = r1 & p [= r1 ) ; then A2: p "/\" p [= r "/\" p by LATTICES:9; assume q in F ; ::_thesis: r "/\" q in F then ex q1 being Element of L st ( q = q1 & p [= q1 ) ; then A3: p "/\" r [= q "/\" r by LATTICES:9; p [= r "/\" q by A3, A2, LATTICES:7; hence r "/\" q in F ; ::_thesis: verum end; now__::_thesis:_for_r,_q_being_Element_of_L_st_r_in_F_&_r_[=_q_holds_ q_in_F let r, q be Element of L; ::_thesis: ( r in F & r [= q implies q in F ) assume r in F ; ::_thesis: ( r [= q implies q in F ) then A4: ex r1 being Element of L st ( r = r1 & p [= r1 ) ; assume r [= q ; ::_thesis: q in F then p [= q by A4, LATTICES:7; hence q in F ; ::_thesis: verum end; hence { q where q is Element of L : p [= q } is Filter of L by A1, Th9; ::_thesis: verum end; end; :: deftheorem defines <. FILTER_0:def_2_:_ for L being Lattice for p being Element of L holds <.p.) = { q where q is Element of L : p [= q } ; theorem Th15: :: FILTER_0:15 for L being Lattice for q, p being Element of L holds ( q in <.p.) iff p [= q ) proof let L be Lattice; ::_thesis: for q, p being Element of L holds ( q in <.p.) iff p [= q ) let q, p be Element of L; ::_thesis: ( q in <.p.) iff p [= q ) ( q in <.p.) iff ex r being Element of L st ( q = r & p [= r ) ) ; hence ( q in <.p.) iff p [= q ) ; ::_thesis: verum end; theorem Th16: :: FILTER_0:16 for L being Lattice for p, q being Element of L holds ( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) ) proof let L be Lattice; ::_thesis: for p, q being Element of L holds ( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) ) let p, q be Element of L; ::_thesis: ( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) ) p [= p "\/" q by LATTICES:5; hence ( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) ) ; ::_thesis: verum end; theorem Th17: :: FILTER_0:17 for L being Lattice st L is 0_Lattice holds <.L.) = <.(Bottom L).) proof let L be Lattice; ::_thesis: ( L is 0_Lattice implies <.L.) = <.(Bottom L).) ) assume L is 0_Lattice ; ::_thesis: <.L.) = <.(Bottom L).) then reconsider L9 = L as 0_Lattice ; thus <.L.) c= <.(Bottom L).) :: according to XBOOLE_0:def_10 ::_thesis: <.(Bottom L).) c= <.L.) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in <.L.) or x in <.(Bottom L).) ) assume x in <.L.) ; ::_thesis: x in <.(Bottom L).) then reconsider x = x as Element of L9 ; ( Bottom L in <.(Bottom L).) & x "/\" (Bottom L9) = Bottom L9 ) ; hence x in <.(Bottom L).) by Th8; ::_thesis: verum end; thus <.(Bottom L).) c= <.L.) ; ::_thesis: verum end; definition let L be Lattice; let F be Filter of L; attrF is being_ultrafilter means :Def3: :: FILTER_0:def 3 ( F <> the carrier of L & ( for H being Filter of L st F c= H & H <> the carrier of L holds F = H ) ); end; :: deftheorem Def3 defines being_ultrafilter FILTER_0:def_3_:_ for L being Lattice for F being Filter of L holds ( F is being_ultrafilter iff ( F <> the carrier of L & ( for H being Filter of L st F c= H & H <> the carrier of L holds F = H ) ) ); theorem Th18: :: FILTER_0:18 for L being Lattice st L is lower-bounded holds for F being Filter of L st F <> the carrier of L holds ex H being Filter of L st ( F c= H & H is being_ultrafilter ) proof let L be Lattice; ::_thesis: ( L is lower-bounded implies for F being Filter of L st F <> the carrier of L holds ex H being Filter of L st ( F c= H & H is being_ultrafilter ) ) given r being Element of L such that A1: for p being Element of L holds ( r "/\" p = r & p "/\" r = r ) ; :: according to LATTICES:def_13 ::_thesis: for F being Filter of L st F <> the carrier of L holds ex H being Filter of L st ( F c= H & H is being_ultrafilter ) A2: for H being Filter of L st r in H holds H = the carrier of L proof let H be Filter of L; ::_thesis: ( r in H implies H = the carrier of L ) assume A3: r in H ; ::_thesis: H = the carrier of L thus H c= the carrier of L ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of L c= H let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of L or x in H ) assume x in the carrier of L ; ::_thesis: x in H then reconsider p = x as Element of L ; r "/\" p = r by A1; then r [= p by LATTICES:4; hence x in H by A3, Th9; ::_thesis: verum end; let F be Filter of L; ::_thesis: ( F <> the carrier of L implies ex H being Filter of L st ( F c= H & H is being_ultrafilter ) ) assume A4: F <> the carrier of L ; ::_thesis: ex H being Filter of L st ( F c= H & H is being_ultrafilter ) set X = { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } ; A5: for x being set st x in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } holds ( x is Subset of L & x is Filter of L ) proof let x be set ; ::_thesis: ( x in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } implies ( x is Subset of L & x is Filter of L ) ) assume x in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } ; ::_thesis: ( x is Subset of L & x is Filter of L ) then ex A being Subset of L st ( x = A & F c= A & A is Filter of L & A <> the carrier of L ) ; hence ( x is Subset of L & x is Filter of L ) ; ::_thesis: verum end; A6: for X1 being set st X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } holds ( F,X1 are_c=-comparable & X1 <> the carrier of L ) proof let X1 be set ; ::_thesis: ( X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } implies ( F,X1 are_c=-comparable & X1 <> the carrier of L ) ) assume X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } ; ::_thesis: ( F,X1 are_c=-comparable & X1 <> the carrier of L ) then ex A being Subset of L st ( X1 = A & F c= A & A is Filter of L & A <> the carrier of L ) ; hence ( F,X1 are_c=-comparable & X1 <> the carrier of L ) by XBOOLE_0:def_9; ::_thesis: verum end; A7: for Z being set st Z c= { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & Z is c=-linear holds ex Y being set st ( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for X1 being set st X1 in Z holds X1 c= Y ) ) proof set x = the Element of F; let Z be set ; ::_thesis: ( Z c= { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & Z is c=-linear implies ex Y being set st ( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for X1 being set st X1 in Z holds X1 c= Y ) ) ) assume that A8: Z c= { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } and A9: Z is c=-linear ; ::_thesis: ex Y being set st ( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for X1 being set st X1 in Z holds X1 c= Y ) ) take Y = union (Z \/ {F}); ::_thesis: ( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for X1 being set st X1 in Z holds X1 c= Y ) ) F in {F} by TARSKI:def_1; then A10: F in Z \/ {F} by XBOOLE_0:def_3; the Element of F in F ; then reconsider V = Y as non empty set by A10, TARSKI:def_4; V c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V or x in the carrier of L ) assume x in V ; ::_thesis: x in the carrier of L then consider X1 being set such that A11: x in X1 and A12: X1 in Z \/ {F} by TARSKI:def_4; ( X1 in Z or X1 in {F} ) by A12, XBOOLE_0:def_3; then X1 is Subset of L by A5, A8; hence x in the carrier of L by A11; ::_thesis: verum end; then reconsider V = V as non empty Subset of L ; now__::_thesis:_for_p,_q_being_Element_of_L_holds_ (_(_p_in_V_&_q_in_V_implies_p_"/\"_q_in_V_)_&_(_p_"/\"_q_in_V_implies_(_p_in_V_&_q_in_V_)_)_) let p, q be Element of L; ::_thesis: ( ( p in V & q in V implies p "/\" q in V ) & ( p "/\" q in V implies ( p in V & q in V ) ) ) thus ( p in V & q in V implies p "/\" q in V ) ::_thesis: ( p "/\" q in V implies ( p in V & q in V ) ) proof assume p in V ; ::_thesis: ( not q in V or p "/\" q in V ) then consider X1 being set such that A13: p in X1 and A14: X1 in Z \/ {F} by TARSKI:def_4; A15: ( X1 in Z or X1 in {F} ) by A14, XBOOLE_0:def_3; then A16: ( ( X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & X1 in Z ) or X1 = F ) by A8, TARSKI:def_1; assume q in V ; ::_thesis: p "/\" q in V then consider X2 being set such that A17: q in X2 and A18: X2 in Z \/ {F} by TARSKI:def_4; A19: ( X2 in Z or X2 in {F} ) by A18, XBOOLE_0:def_3; then ( ( X2 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & X2 in Z ) or X2 = F ) by A8, TARSKI:def_1; then X1,X2 are_c=-comparable by A6, A9, A16, ORDINAL1:def_8; then A20: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9; A21: X1 is Filter of L by A5, A8, A15, TARSKI:def_1; X2 is Filter of L by A5, A8, A19, TARSKI:def_1; then ( p "/\" q in X1 or p "/\" q in X2 ) by A13, A17, A20, A21, Th9; hence p "/\" q in V by A14, A18, TARSKI:def_4; ::_thesis: verum end; assume p "/\" q in V ; ::_thesis: ( p in V & q in V ) then consider X1 being set such that A22: p "/\" q in X1 and A23: X1 in Z \/ {F} by TARSKI:def_4; ( X1 in Z or X1 in {F} ) by A23, XBOOLE_0:def_3; then X1 is Filter of L by A5, A8, TARSKI:def_1; then ( p in X1 & q in X1 ) by A22, Th8; hence ( p in V & q in V ) by A23, TARSKI:def_4; ::_thesis: verum end; then reconsider V = V as Filter of L by Th8; now__::_thesis:_not_r_in_V assume r in V ; ::_thesis: contradiction then consider X1 being set such that A24: r in X1 and A25: X1 in Z \/ {F} by TARSKI:def_4; ( X1 in Z or X1 in {F} ) by A25, XBOOLE_0:def_3; then ( X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } or X1 = F ) by A8, TARSKI:def_1; then ex A being Subset of L st ( X1 = A & F c= A & A is Filter of L & A <> the carrier of L ) by A4; hence contradiction by A2, A24; ::_thesis: verum end; then A26: V <> the carrier of L ; F c= V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in V ) thus ( not x in F or x in V ) by A10, TARSKI:def_4; ::_thesis: verum end; hence Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } by A26; ::_thesis: for X1 being set st X1 in Z holds X1 c= Y let X1 be set ; ::_thesis: ( X1 in Z implies X1 c= Y ) assume X1 in Z ; ::_thesis: X1 c= Y then X1 in Z \/ {F} by XBOOLE_0:def_3; hence X1 c= Y by ZFMISC_1:74; ::_thesis: verum end; F in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } by A4; then consider Y being set such that A27: Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } and A28: for Z being set st Z in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & Z <> Y holds not Y c= Z by A7, ORDERS_1:65; consider H being Subset of L such that A29: Y = H and A30: F c= H and A31: H is Filter of L and A32: H <> the carrier of L by A27; reconsider H = H as Filter of L by A31; take H ; ::_thesis: ( F c= H & H is being_ultrafilter ) thus ( F c= H & H <> the carrier of L ) by A30, A32; :: according to FILTER_0:def_3 ::_thesis: for H being Filter of L st H c= H & H <> the carrier of L holds H = H let G be Filter of L; ::_thesis: ( H c= G & G <> the carrier of L implies H = G ) assume that A33: H c= G and A34: G <> the carrier of L ; ::_thesis: H = G F c= G by A30, A33, XBOOLE_1:1; then G in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } by A34; hence H = G by A28, A29, A33; ::_thesis: verum end; theorem Th19: :: FILTER_0:19 for L being Lattice for p being Element of L st ex r being Element of L st p "/\" r <> p holds <.p.) <> the carrier of L proof let L be Lattice; ::_thesis: for p being Element of L st ex r being Element of L st p "/\" r <> p holds <.p.) <> the carrier of L let p be Element of L; ::_thesis: ( ex r being Element of L st p "/\" r <> p implies <.p.) <> the carrier of L ) given r being Element of L such that A1: p "/\" r <> p ; ::_thesis: <.p.) <> the carrier of L p "/\" r [= p by LATTICES:6; then not p [= p "/\" r by A1, LATTICES:8; hence <.p.) <> the carrier of L by Th15; ::_thesis: verum end; theorem Th20: :: FILTER_0:20 for L being Lattice for p being Element of L st L is 0_Lattice & p <> Bottom L holds ex H being Filter of L st ( p in H & H is being_ultrafilter ) proof let L be Lattice; ::_thesis: for p being Element of L st L is 0_Lattice & p <> Bottom L holds ex H being Filter of L st ( p in H & H is being_ultrafilter ) let p be Element of L; ::_thesis: ( L is 0_Lattice & p <> Bottom L implies ex H being Filter of L st ( p in H & H is being_ultrafilter ) ) assume that A1: L is 0_Lattice and A2: p <> Bottom L ; ::_thesis: ex H being Filter of L st ( p in H & H is being_ultrafilter ) reconsider L9 = L as 0_Lattice by A1; reconsider p9 = p as Element of L9 ; p9 "/\" (Bottom L9) = Bottom L9 ; then consider H being Filter of L such that A3: ( <.p.) c= H & H is being_ultrafilter ) by A2, Th18, Th19; take H ; ::_thesis: ( p in H & H is being_ultrafilter ) p in <.p.) ; hence ( p in H & H is being_ultrafilter ) by A3; ::_thesis: verum end; definition let L be Lattice; let D be non empty Subset of L; func<.D.) -> Filter of L means :Def4: :: FILTER_0:def 4 ( D c= it & ( for F being Filter of L st D c= F holds it c= F ) ); existence ex b1 being Filter of L st ( D c= b1 & ( for F being Filter of L st D c= F holds b1 c= F ) ) proof set x = the Element of D; defpred S1[ set ] means ( \$1 is Filter of L & D c= \$1 ); consider X being set such that A1: for Z being set holds ( Z in X iff ( Z in bool the carrier of L & S1[Z] ) ) from XBOOLE_0:sch_1(); reconsider x = the Element of D as Element of L ; <.L.) = the carrier of L ; then A2: X <> {} by A1; now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_ x_in_Z let Z be set ; ::_thesis: ( Z in X implies x in Z ) assume Z in X ; ::_thesis: x in Z then D c= Z by A1; hence x in Z by TARSKI:def_3; ::_thesis: verum end; then reconsider F = meet X as non empty set by A2, SETFAM_1:def_1; A3: <.L.) in X by A1; F c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in the carrier of L ) thus ( not x in F or x in the carrier of L ) by A3, SETFAM_1:def_1; ::_thesis: verum end; then reconsider F = F as non empty Subset of L ; now__::_thesis:_for_p,_q_being_Element_of_L_holds_ (_(_p_in_F_&_q_in_F_implies_p_"/\"_q_in_F_)_&_(_p_"/\"_q_in_F_implies_(_p_in_F_&_q_in_F_)_)_) let p, q be Element of L; ::_thesis: ( ( p in F & q in F implies p "/\" q in F ) & ( p "/\" q in F implies ( p in F & q in F ) ) ) thus ( p in F & q in F implies p "/\" q in F ) ::_thesis: ( p "/\" q in F implies ( p in F & q in F ) ) proof assume A4: ( p in F & q in F ) ; ::_thesis: p "/\" q in F for Z being set st Z in X holds p "/\" q in Z proof let Z be set ; ::_thesis: ( Z in X implies p "/\" q in Z ) assume A5: Z in X ; ::_thesis: p "/\" q in Z then reconsider Z9 = Z as Filter of L by A1; ( p in Z9 & q in Z9 ) by A4, A5, SETFAM_1:def_1; hence p "/\" q in Z by Th8; ::_thesis: verum end; hence p "/\" q in F by A2, SETFAM_1:def_1; ::_thesis: verum end; assume A6: p "/\" q in F ; ::_thesis: ( p in F & q in F ) now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_ p_in_Z let Z be set ; ::_thesis: ( Z in X implies p in Z ) assume A7: Z in X ; ::_thesis: p in Z then reconsider Z9 = Z as Filter of L by A1; p "/\" q in Z9 by A6, A7, SETFAM_1:def_1; hence p in Z by Th8; ::_thesis: verum end; hence p in F by A2, SETFAM_1:def_1; ::_thesis: q in F now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_ q_in_Z let Z be set ; ::_thesis: ( Z in X implies q in Z ) assume A8: Z in X ; ::_thesis: q in Z then reconsider Z9 = Z as Filter of L by A1; p "/\" q in Z9 by A6, A8, SETFAM_1:def_1; hence q in Z by Th8; ::_thesis: verum end; hence q in F by A2, SETFAM_1:def_1; ::_thesis: verum end; then reconsider F = F as Filter of L by Th8; take F ; ::_thesis: ( D c= F & ( for F being Filter of L st D c= F holds F c= F ) ) for Z being set st Z in X holds D c= Z by A1; hence D c= F by A2, SETFAM_1:5; ::_thesis: for F being Filter of L st D c= F holds F c= F let H be Filter of L; ::_thesis: ( D c= H implies F c= H ) assume D c= H ; ::_thesis: F c= H then H in X by A1; hence F c= H by SETFAM_1:3; ::_thesis: verum end; uniqueness for b1, b2 being Filter of L st D c= b1 & ( for F being Filter of L st D c= F holds b1 c= F ) & D c= b2 & ( for F being Filter of L st D c= F holds b2 c= F ) holds b1 = b2 proof let F1, F2 be Filter of L; ::_thesis: ( D c= F1 & ( for F being Filter of L st D c= F holds F1 c= F ) & D c= F2 & ( for F being Filter of L st D c= F holds F2 c= F ) implies F1 = F2 ) assume ( D c= F1 & ( for F being Filter of L st D c= F holds F1 c= F ) & D c= F2 & ( for F being Filter of L st D c= F holds F2 c= F ) ) ; ::_thesis: F1 = F2 hence ( F1 c= F2 & F2 c= F1 ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum end; end; :: deftheorem Def4 defines <. FILTER_0:def_4_:_ for L being Lattice for D being non empty Subset of L for b3 being Filter of L holds ( b3 = <.D.) iff ( D c= b3 & ( for F being Filter of L st D c= F holds b3 c= F ) ) ); theorem Th21: :: FILTER_0:21 for L being Lattice for F being Filter of L holds <.F.) = F proof let L be Lattice; ::_thesis: for F being Filter of L holds <.F.) = F let F be Filter of L; ::_thesis: <.F.) = F for H being Filter of L st F c= H holds F c= H ; hence <.F.) = F by Def4; ::_thesis: verum end; theorem Th22: :: FILTER_0:22 for L being Lattice for D1, D2 being non empty Subset of L st D1 c= D2 holds <.D1.) c= <.D2.) proof let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L st D1 c= D2 holds <.D1.) c= <.D2.) let D1, D2 be non empty Subset of L; ::_thesis: ( D1 c= D2 implies <.D1.) c= <.D2.) ) assume A1: D1 c= D2 ; ::_thesis: <.D1.) c= <.D2.) D2 c= <.D2.) by Def4; then D1 c= <.D2.) by A1, XBOOLE_1:1; hence <.D1.) c= <.D2.) by Def4; ::_thesis: verum end; theorem Th23: :: FILTER_0:23 for L being Lattice for p being Element of L for D being non empty Subset of L st p in D holds <.p.) c= <.D.) proof let L be Lattice; ::_thesis: for p being Element of L for D being non empty Subset of L st p in D holds <.p.) c= <.D.) let p be Element of L; ::_thesis: for D being non empty Subset of L st p in D holds <.p.) c= <.D.) let D be non empty Subset of L; ::_thesis: ( p in D implies <.p.) c= <.D.) ) assume A1: p in D ; ::_thesis: <.p.) c= <.D.) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in <.p.) or x in <.D.) ) A2: D c= <.D.) by Def4; assume x in <.p.) ; ::_thesis: x in <.D.) then ex q being Element of L st ( x = q & p [= q ) ; hence x in <.D.) by A1, A2, Th9; ::_thesis: verum end; theorem Th24: :: FILTER_0:24 for L being Lattice for p being Element of L for D being non empty Subset of L st D = {p} holds <.D.) = <.p.) proof let L be Lattice; ::_thesis: for p being Element of L for D being non empty Subset of L st D = {p} holds <.D.) = <.p.) let p be Element of L; ::_thesis: for D being non empty Subset of L st D = {p} holds <.D.) = <.p.) let D be non empty Subset of L; ::_thesis: ( D = {p} implies <.D.) = <.p.) ) assume A1: D = {p} ; ::_thesis: <.D.) = <.p.) D c= <.p.) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in <.p.) ) assume x in D ; ::_thesis: x in <.p.) then x = p by A1, TARSKI:def_1; hence x in <.p.) ; ::_thesis: verum end; hence <.D.) c= <.p.) by Def4; :: according to XBOOLE_0:def_10 ::_thesis: <.p.) c= <.D.) p in D by A1, TARSKI:def_1; hence <.p.) c= <.D.) by Th23; ::_thesis: verum end; theorem Th25: :: FILTER_0:25 for L being Lattice for D being non empty Subset of L st L is 0_Lattice & Bottom L in D holds ( <.D.) = <.L.) & <.D.) = the carrier of L ) proof let L be Lattice; ::_thesis: for D being non empty Subset of L st L is 0_Lattice & Bottom L in D holds ( <.D.) = <.L.) & <.D.) = the carrier of L ) let D be non empty Subset of L; ::_thesis: ( L is 0_Lattice & Bottom L in D implies ( <.D.) = <.L.) & <.D.) = the carrier of L ) ) assume that A1: L is 0_Lattice and A2: Bottom L in D ; ::_thesis: ( <.D.) = <.L.) & <.D.) = the carrier of L ) A3: <.(Bottom L).) = <.L.) by A1, Th17; hence ( <.D.) c= <.L.) & <.L.) c= <.D.) ) by A2, Th23; :: according to XBOOLE_0:def_10 ::_thesis: <.D.) = the carrier of L thus ( <.D.) c= the carrier of L & the carrier of L c= <.D.) ) by A2, A3, Th23; :: according to XBOOLE_0:def_10 ::_thesis: verum end; theorem Th26: :: FILTER_0:26 for L being Lattice for F being Filter of L st L is 0_Lattice & Bottom L in F holds ( F = <.L.) & F = the carrier of L ) proof let L be Lattice; ::_thesis: for F being Filter of L st L is 0_Lattice & Bottom L in F holds ( F = <.L.) & F = the carrier of L ) let F be Filter of L; ::_thesis: ( L is 0_Lattice & Bottom L in F implies ( F = <.L.) & F = the carrier of L ) ) F = <.F.) by Th21; hence ( L is 0_Lattice & Bottom L in F implies ( F = <.L.) & F = the carrier of L ) ) by Th25; ::_thesis: verum end; definition let L be Lattice; let F be Filter of L; attrF is prime means :: FILTER_0:def 5 for p, q being Element of L holds ( p "\/" q in F iff ( p in F or q in F ) ); end; :: deftheorem defines prime FILTER_0:def_5_:_ for L being Lattice for F being Filter of L holds ( F is prime iff for p, q being Element of L holds ( p "\/" q in F iff ( p in F or q in F ) ) ); theorem Th27: :: FILTER_0:27 for L being Lattice st L is B_Lattice holds for p, q being Element of L holds ( p "/\" ((p `) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds r [= (p `) "\/" q ) ) proof let L be Lattice; ::_thesis: ( L is B_Lattice implies for p, q being Element of L holds ( p "/\" ((p `) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds r [= (p `) "\/" q ) ) ) assume L is B_Lattice ; ::_thesis: for p, q being Element of L holds ( p "/\" ((p `) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds r [= (p `) "\/" q ) ) then reconsider S = L as B_Lattice ; reconsider J = S as 1_Lattice ; reconsider K = S as 0_Lattice ; let p, q be Element of L; ::_thesis: ( p "/\" ((p `) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds r [= (p `) "\/" q ) ) set r = (p `) "\/" q; reconsider p9 = p, q9 = q as Element of K ; reconsider p99 = p as Element of S ; A1: ( p99 "/\" (p99 `) = Bottom L & (Bottom K) "\/" (p9 "/\" q9) = p9 "/\" q9 ) by LATTICES:20; reconsider K = S as D_Lattice ; reconsider p9 = p, q9 = q, r9 = (p `) "\/" q as Element of K ; p9 "/\" r9 = (p9 "/\" (p9 `)) "\/" (p9 "/\" q9) by LATTICES:def_11; hence p "/\" ((p `) "\/" q) [= q by A1, LATTICES:6; ::_thesis: for r being Element of L st p "/\" r [= q holds r [= (p `) "\/" q let r1 be Element of L; ::_thesis: ( p "/\" r1 [= q implies r1 [= (p `) "\/" q ) reconsider r19 = r1 as Element of K ; reconsider pp = p, r99 = r1 as Element of J ; A2: ( (p99 `) "\/" p99 = Top L & (Top J) "/\" ((pp `) "\/" r99) = (pp `) "\/" r99 ) by LATTICES:21; assume p "/\" r1 [= q ; ::_thesis: r1 [= (p `) "\/" q then A3: (p `) "\/" (p "/\" r1) [= (p `) "\/" q by Th1; ( (p9 `) "\/" (p9 "/\" r19) = ((p9 `) "\/" p9) "/\" ((p9 `) "\/" r19) & r1 [= r1 "\/" (p `) ) by LATTICES:5, LATTICES:11; hence r1 [= (p `) "\/" q by A3, A2, LATTICES:7; ::_thesis: verum end; definition let IT be non empty LattStr ; attrIT is implicative means :Def6: :: FILTER_0:def 6 for p, q being Element of IT ex r being Element of IT st ( p "/\" r [= q & ( for r1 being Element of IT st p "/\" r1 [= q holds r1 [= r ) ); end; :: deftheorem Def6 defines implicative FILTER_0:def_6_:_ for IT being non empty LattStr holds ( IT is implicative iff for p, q being Element of IT ex r being Element of IT st ( p "/\" r [= q & ( for r1 being Element of IT st p "/\" r1 [= q holds r1 [= r ) ) ); registration cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like implicative for LattStr ; existence ex b1 being Lattice st ( b1 is strict & b1 is implicative ) proof set L = the strict B_Lattice; now__::_thesis:_for_p,_q_being_Element_of_the_strict_B_Lattice_ex_r_being_Element_of_the_strict_B_Lattice_st_ (_p_"/\"_r_[=_q_&_(_for_r1_being_Element_of_the_strict_B_Lattice_st_p_"/\"_r1_[=_q_holds_ r1_[=_r_)_) let p, q be Element of the strict B_Lattice; ::_thesis: ex r being Element of the strict B_Lattice st ( p "/\" r [= q & ( for r1 being Element of the strict B_Lattice st p "/\" r1 [= q holds r1 [= r ) ) reconsider r = (p `) "\/" q as Element of the strict B_Lattice ; take r = r; ::_thesis: ( p "/\" r [= q & ( for r1 being Element of the strict B_Lattice st p "/\" r1 [= q holds r1 [= r ) ) thus ( p "/\" r [= q & ( for r1 being Element of the strict B_Lattice st p "/\" r1 [= q holds r1 [= r ) ) by Th27; ::_thesis: verum end; then the strict B_Lattice is implicative by Def6; hence ex b1 being Lattice st ( b1 is strict & b1 is implicative ) ; ::_thesis: verum end; end; definition mode I_Lattice is implicative Lattice; end; definition let L be Lattice; let p, q be Element of L; assume A1: L is I_Lattice ; funcp => q -> Element of L means :Def7: :: FILTER_0:def 7 ( p "/\" it [= q & ( for r being Element of L st p "/\" r [= q holds r [= it ) ); existence ex b1 being Element of L st ( p "/\" b1 [= q & ( for r being Element of L st p "/\" r [= q holds r [= b1 ) ) by A1, Def6; correctness uniqueness for b1, b2 being Element of L st p "/\" b1 [= q & ( for r being Element of L st p "/\" r [= q holds r [= b1 ) & p "/\" b2 [= q & ( for r being Element of L st p "/\" r [= q holds r [= b2 ) holds b1 = b2; proof let r1, r2 be Element of L; ::_thesis: ( p "/\" r1 [= q & ( for r being Element of L st p "/\" r [= q holds r [= r1 ) & p "/\" r2 [= q & ( for r being Element of L st p "/\" r [= q holds r [= r2 ) implies r1 = r2 ) assume ( p "/\" r1 [= q & ( for r being Element of L st p "/\" r [= q holds r [= r1 ) & p "/\" r2 [= q & ( for r being Element of L st p "/\" r [= q holds r [= r2 ) ) ; ::_thesis: r1 = r2 then ( r1 [= r2 & r2 [= r1 ) ; hence r1 = r2 by LATTICES:8; ::_thesis: verum end; end; :: deftheorem Def7 defines => FILTER_0:def_7_:_ for L being Lattice for p, q being Element of L st L is I_Lattice holds for b4 being Element of L holds ( b4 = p => q iff ( p "/\" b4 [= q & ( for r being Element of L st p "/\" r [= q holds r [= b4 ) ) ); registration cluster non empty Lattice-like implicative -> upper-bounded for LattStr ; coherence for b1 being I_Lattice holds b1 is upper-bounded proof let I be I_Lattice; ::_thesis: I is upper-bounded set i = the Element of I; take k = the Element of I => the Element of I; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of I holds ( k "\/" b1 = k & b1 "\/" k = k ) let j be Element of I; ::_thesis: ( k "\/" j = k & j "\/" k = k ) the Element of I "/\" j [= the Element of I by LATTICES:6; then A1: j [= k by Def7; j "\/" k = k "\/" j ; hence ( k "\/" j = k & j "\/" k = k ) by A1, LATTICES:def_3; ::_thesis: verum end; end; theorem Th28: :: FILTER_0:28 for I being I_Lattice for i being Element of I holds i => i = Top I proof let I be I_Lattice; ::_thesis: for i being Element of I holds i => i = Top I let i be Element of I; ::_thesis: i => i = Top I now__::_thesis:_for_j_being_Element_of_I_holds_j_"\/"_(i_=>_i)_=_i_=>_i let j be Element of I; ::_thesis: j "\/" (i => i) = i => i i "/\" j [= i by LATTICES:6; then j [= i => i by Def7; hence j "\/" (i => i) = i => i by LATTICES:def_3; ::_thesis: verum end; hence i => i = Top I by RLSUB_2:65; ::_thesis: verum end; registration cluster non empty Lattice-like implicative -> distributive for LattStr ; coherence for b1 being I_Lattice holds b1 is distributive proof let I be I_Lattice; ::_thesis: I is distributive let i be Element of I; :: according to LATTICES:def_11 ::_thesis: for b1, b2 being Element of the carrier of I holds i "/\" (b1 "\/" b2) = (i "/\" b1) "\/" (i "/\" b2) let j, k be Element of I; ::_thesis: i "/\" (j "\/" k) = (i "/\" j) "\/" (i "/\" k) i "/\" k [= (i "/\" k) "\/" (i "/\" j) by LATTICES:5; then A1: k [= i => ((i "/\" j) "\/" (i "/\" k)) by Def7; i "/\" j [= (i "/\" j) "\/" (i "/\" k) by LATTICES:5; then j [= i => ((i "/\" j) "\/" (i "/\" k)) by Def7; then j "\/" k [= i => ((i "/\" j) "\/" (i "/\" k)) by A1, Th6; then A2: i "/\" (j "\/" k) [= i "/\" (i => ((i "/\" j) "\/" (i "/\" k))) by LATTICES:9; ( i "/\" j [= i "/\" (j "\/" k) & i "/\" k [= i "/\" (j "\/" k) ) by LATTICES:5, LATTICES:9; then A3: (i "/\" j) "\/" (i "/\" k) [= i "/\" (j "\/" k) by Th6; i "/\" (i => ((i "/\" j) "\/" (i "/\" k))) [= (i "/\" j) "\/" (i "/\" k) by Def7; then i "/\" (j "\/" k) [= (i "/\" j) "\/" (i "/\" k) by A2, LATTICES:7; hence i "/\" (j "\/" k) = (i "/\" j) "\/" (i "/\" k) by A3, LATTICES:8; ::_thesis: verum end; end; registration cluster non empty Lattice-like Boolean -> implicative for LattStr ; coherence for b1 being B_Lattice holds b1 is implicative proof let B be B_Lattice; ::_thesis: B is implicative let p, q be Element of B; :: according to FILTER_0:def_6 ::_thesis: ex r being Element of B st ( p "/\" r [= q & ( for r1 being Element of B st p "/\" r1 [= q holds r1 [= r ) ) take r = (p `) "\/" q; ::_thesis: ( p "/\" r [= q & ( for r1 being Element of B st p "/\" r1 [= q holds r1 [= r ) ) thus ( p "/\" r [= q & ( for r1 being Element of B st p "/\" r1 [= q holds r1 [= r ) ) by Th27; ::_thesis: verum end; end; registration cluster non empty Lattice-like implicative -> distributive for LattStr ; coherence for b1 being Lattice st b1 is implicative holds b1 is distributive ; end; theorem Th29: :: FILTER_0:29 for I being I_Lattice for i, j being Element of I for FI being Filter of I st i in FI & i => j in FI holds j in FI proof let I be I_Lattice; ::_thesis: for i, j being Element of I for FI being Filter of I st i in FI & i => j in FI holds j in FI let i, j be Element of I; ::_thesis: for FI being Filter of I st i in FI & i => j in FI holds j in FI let FI be Filter of I; ::_thesis: ( i in FI & i => j in FI implies j in FI ) assume ( i in FI & i => j in FI ) ; ::_thesis: j in FI then A1: i "/\" (i => j) in FI by Th8; i "/\" (i => j) [= j by Def7; hence j in FI by A1, Th9; ::_thesis: verum end; theorem Th30: :: FILTER_0:30 for I being I_Lattice for j, i being Element of I for FI being Filter of I st j in FI holds i => j in FI proof let I be I_Lattice; ::_thesis: for j, i being Element of I for FI being Filter of I st j in FI holds i => j in FI let j, i be Element of I; ::_thesis: for FI being Filter of I st j in FI holds i => j in FI let FI be Filter of I; ::_thesis: ( j in FI implies i => j in FI ) j "/\" i [= j by LATTICES:6; then j [= i => j by Def7; hence ( j in FI implies i => j in FI ) by Th9; ::_thesis: verum end; definition let L be Lattice; let D1, D2 be non empty Subset of L; funcD1 "/\" D2 -> Subset of L equals :: FILTER_0:def 8 { (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ; coherence { (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } is Subset of L proof set x = the Element of D1; set y = the Element of D2; reconsider x = the Element of D1, y = the Element of D2 as Element of L ; x "/\" y in { (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ; then reconsider D = { (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } as non empty set ; D c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in the carrier of L ) assume x in D ; ::_thesis: x in the carrier of L then ex p, q being Element of L st ( x = p "/\" q & p in D1 & q in D2 ) ; hence x in the carrier of L ; ::_thesis: verum end; hence { (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } is Subset of L ; ::_thesis: verum end; end; :: deftheorem defines "/\" FILTER_0:def_8_:_ for L being Lattice for D1, D2 being non empty Subset of L holds D1 "/\" D2 = { (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ; registration let L be Lattice; let D1, D2 be non empty Subset of L; clusterD1 "/\" D2 -> non empty ; coherence not D1 "/\" D2 is empty proof set x = the Element of D1; set y = the Element of D2; reconsider x = the Element of D1, y = the Element of D2 as Element of L ; x "/\" y in { (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ; hence not D1 "/\" D2 is empty ; ::_thesis: verum end; end; theorem :: FILTER_0:31 for L being Lattice for p, q being Element of L for D1, D2 being non empty Subset of L st p in D1 & q in D2 holds ( p "/\" q in D1 "/\" D2 & q "/\" p in D1 "/\" D2 ) ; theorem :: FILTER_0:32 for L being Lattice for x being set for D1, D2 being non empty Subset of L st x in D1 "/\" D2 holds ex p, q being Element of L st ( x = p "/\" q & p in D1 & q in D2 ) ; theorem Th33: :: FILTER_0:33 for L being Lattice for D1, D2 being non empty Subset of L holds D1 "/\" D2 = D2 "/\" D1 proof let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L holds D1 "/\" D2 = D2 "/\" D1 let D1, D2 be non empty Subset of L; ::_thesis: D1 "/\" D2 = D2 "/\" D1 now__::_thesis:_for_D1,_D2_being_non_empty_Subset_of_L_holds_D1_"/\"_D2_c=_D2_"/\"_D1 let D1, D2 be non empty Subset of L; ::_thesis: D1 "/\" D2 c= D2 "/\" D1 thus D1 "/\" D2 c= D2 "/\" D1 ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 "/\" D2 or x in D2 "/\" D1 ) assume x in D1 "/\" D2 ; ::_thesis: x in D2 "/\" D1 then ex p, q being Element of L st ( x = p "/\" q & p in D1 & q in D2 ) ; hence x in D2 "/\" D1 ; ::_thesis: verum end; end; hence ( D1 "/\" D2 c= D2 "/\" D1 & D2 "/\" D1 c= D1 "/\" D2 ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum end; registration let L be D_Lattice; let F1, F2 be Filter of L; clusterF1 "/\" F2 -> final meet-closed ; coherence ( F1 "/\" F2 is final & F1 "/\" F2 is meet-closed ) proof now__::_thesis:_for_p,_q_being_Element_of_L_holds_ (_(_p_in_F1_"/\"_F2_&_q_in_F1_"/\"_F2_implies_p_"/\"_q_in_F1_"/\"_F2_)_&_(_p_"/\"_q_in_F1_"/\"_F2_implies_(_p_in_F1_"/\"_F2_&_q_in_F1_"/\"_F2_)_)_) let p, q be Element of L; ::_thesis: ( ( p in F1 "/\" F2 & q in F1 "/\" F2 implies p "/\" q in F1 "/\" F2 ) & ( p "/\" q in F1 "/\" F2 implies ( p in F1 "/\" F2 & q in F1 "/\" F2 ) ) ) A1: ( p = p "\/" (p "/\" q) & q = q "\/" (p "/\" q) ) by LATTICES:def_8; thus ( p in F1 "/\" F2 & q in F1 "/\" F2 implies p "/\" q in F1 "/\" F2 ) ::_thesis: ( p "/\" q in F1 "/\" F2 implies ( p in F1 "/\" F2 & q in F1 "/\" F2 ) ) proof assume p in F1 "/\" F2 ; ::_thesis: ( not q in F1 "/\" F2 or p "/\" q in F1 "/\" F2 ) then consider p1, p2 being Element of L such that A2: p = p1 "/\" p2 and A3: ( p1 in F1 & p2 in F2 ) ; assume q in F1 "/\" F2 ; ::_thesis: p "/\" q in F1 "/\" F2 then consider q1, q2 being Element of L such that A4: q = q1 "/\" q2 and A5: ( q1 in F1 & q2 in F2 ) ; A6: p "/\" q = ((p1 "/\" p2) "/\" q1) "/\" q2 by A2, A4, LATTICES:def_7 .= ((p1 "/\" q1) "/\" p2) "/\" q2 by LATTICES:def_7 .= (p1 "/\" q1) "/\" (p2 "/\" q2) by LATTICES:def_7 ; ( p1 "/\" q1 in F1 & p2 "/\" q2 in F2 ) by A3, A5, Th8; hence p "/\" q in F1 "/\" F2 by A6; ::_thesis: verum end; assume p "/\" q in F1 "/\" F2 ; ::_thesis: ( p in F1 "/\" F2 & q in F1 "/\" F2 ) then consider p1, q1 being Element of L such that A7: p "/\" q = p1 "/\" q1 and A8: ( p1 in F1 & q1 in F2 ) ; A9: ( q "\/" p1 in F1 & q "\/" q1 in F2 ) by A8, Th10; A10: ( p "\/" (p1 "/\" q1) = (p "\/" p1) "/\" (p "\/" q1) & q "\/" (p1 "/\" q1) = (q "\/" p1) "/\" (q "\/" q1) ) by LATTICES:11; ( p "\/" p1 in F1 & p "\/" q1 in F2 ) by A8, Th10; hence ( p in F1 "/\" F2 & q in F1 "/\" F2 ) by A7, A1, A10, A9; ::_thesis: verum end; hence ( F1 "/\" F2 is final & F1 "/\" F2 is meet-closed ) by Th8; ::_thesis: verum end; end; theorem Th34: :: FILTER_0:34 for L being Lattice for D1, D2 being non empty Subset of L holds ( <.(D1 \/ D2).) = <.(<.D1.) \/ D2).) & <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).) ) proof let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L holds ( <.(D1 \/ D2).) = <.(<.D1.) \/ D2).) & <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).) ) let D1, D2 be non empty Subset of L; ::_thesis: ( <.(D1 \/ D2).) = <.(<.D1.) \/ D2).) & <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).) ) now__::_thesis:_for_D1,_D2_being_non_empty_Subset_of_L_holds_ (_<.(D1_\/_D2).)_c=_<.(<.D1.)_\/_D2).)_&_<.(<.D1.)_\/_D2).)_c=_<.(D1_\/_D2).)_) let D1, D2 be non empty Subset of L; ::_thesis: ( <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) & <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) ) ( D2 c= D1 \/ D2 & D1 \/ D2 c= <.(D1 \/ D2).) ) by Def4, XBOOLE_1:7; then A1: D2 c= <.(D1 \/ D2).) by XBOOLE_1:1; D1 c= <.D1.) by Def4; then D1 \/ D2 c= <.D1.) \/ D2 by XBOOLE_1:9; hence <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) by Th22; ::_thesis: <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) <.D1.) c= <.(D1 \/ D2).) by Th22, XBOOLE_1:7; then <.D1.) \/ D2 c= <.(D1 \/ D2).) by A1, XBOOLE_1:8; hence <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) by Def4; ::_thesis: verum end; hence ( <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) & <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) & <.(D1 \/ D2).) c= <.(D1 \/ <.D2.)).) & <.(D1 \/ <.D2.)).) c= <.(D1 \/ D2).) ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum end; theorem :: FILTER_0:35 for L being Lattice for F, H being Filter of L holds <.(F \/ H).) = { r where r is Element of L : ex p, q being Element of L st ( p "/\" q [= r & p in F & q in H ) } proof let L be Lattice; ::_thesis: for F, H being Filter of L holds <.(F \/ H).) = { r where r is Element of L : ex p, q being Element of L st ( p "/\" q [= r & p in F & q in H ) } let F, H be Filter of L; ::_thesis: <.(F \/ H).) = { r where r is Element of L : ex p, q being Element of L st ( p "/\" q [= r & p in F & q in H ) } set X = { r1 where r1 is Element of L : ex p, q being Element of L st ( p "/\" q [= r1 & p in F & q in H ) } ; consider p1 being Element of L such that A1: p1 in F by SUBSET_1:4; consider q1 being Element of L such that A2: q1 in H by SUBSET_1:4; p1 "/\" q1 in { r1 where r1 is Element of L : ex p, q being Element of L st ( p "/\" q [= r1 & p in F & q in H ) } by A1, A2; then reconsider D = { r1 where r1 is Element of L : ex p, q being Element of L st ( p "/\" q [= r1 & p in F & q in H ) } as non empty set ; D c= the carrier of L proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in the carrier of L ) assume x in D ; ::_thesis: x in the carrier of L then ex r1 being Element of L st ( x = r1 & ex p, q being Element of L st ( p "/\" q [= r1 & p in F & q in H ) ) ; hence x in the carrier of L ; ::_thesis: verum end; then reconsider D = D as non empty Subset of L ; A3: for p, q being Element of L st p in D & p [= q holds q in D proof let p, q be Element of L; ::_thesis: ( p in D & p [= q implies q in D ) assume p in D ; ::_thesis: ( not p [= q or q in D ) then ex r1 being Element of L st ( p = r1 & ex p, q being Element of L st ( p "/\" q [= r1 & p in F & q in H ) ) ; then consider p1, q1 being Element of L such that A4: p1 "/\" q1 [= p and A5: ( p1 in F & q1 in H ) ; assume p [= q ; ::_thesis: q in D then p1 "/\" q1 [= q by A4, LATTICES:7; hence q in D by A5; ::_thesis: verum end; for p, q being Element of L st p in D & q in D holds p "/\" q in D proof let p, q be Element of L; ::_thesis: ( p in D & q in D implies p "/\" q in D ) assume p in D ; ::_thesis: ( not q in D or p "/\" q in D ) then ex r1 being Element of L st ( p = r1 & ex p, q being Element of L st ( p "/\" q [= r1 & p in F & q in H ) ) ; then consider p1, q1 being Element of L such that A6: p1 "/\" q1 [= p and A7: ( p1 in F & q1 in H ) ; assume q in D ; ::_thesis: p "/\" q in D then ex r2 being Element of L st ( q = r2 & ex p, q being Element of L st ( p "/\" q [= r2 & p in F & q in H ) ) ; then consider p2, q2 being Element of L such that A8: p2 "/\" q2 [= q and A9: ( p2 in F & q2 in H ) ; A10: p "/\" (p2 "/\" q2) [= p "/\" q by A8, LATTICES:9; (p1 "/\" q1) "/\" (p2 "/\" q2) [= p "/\" (p2 "/\" q2) by A6, LATTICES:9; then A11: (p1 "/\" q1) "/\" (p2 "/\" q2) [= p "/\" q by A10, LATTICES:7; A12: (p1 "/\" q1) "/\" (p2 "/\" q2) = ((p1 "/\" q1) "/\" p2) "/\" q2 by LATTICES:def_7 .= ((p1 "/\" p2) "/\" q1) "/\" q2 by LATTICES:def_7 .= (p1 "/\" p2) "/\" (q1 "/\" q2) by LATTICES:def_7 ; ( p1 "/\" p2 in F & q1 "/\" q2 in H ) by A7, A9, Th8; hence p "/\" q in D by A12, A11; ::_thesis: verum end; then reconsider D = D as Filter of L by A3, Th9; A13: H c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H or x in D ) assume x in H ; ::_thesis: x in D then reconsider q = x as Element of H ; q "/\" p1 [= q by LATTICES:6; hence x in D by A1; ::_thesis: verum end; F c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in D ) assume x in F ; ::_thesis: x in D then reconsider p = x as Element of F ; p "/\" q1 [= p by LATTICES:6; hence x in D by A2; ::_thesis: verum end; then F \/ H c= D by A13, XBOOLE_1:8; hence <.(F \/ H).) c= { r1 where r1 is Element of L : ex p, q being Element of L st ( p "/\" q [= r1 & p in F & q in H ) } by Def4; :: according to XBOOLE_0:def_10 ::_thesis: { r where r is Element of L : ex p, q being Element of L st ( p "/\" q [= r & p in F & q in H ) } c= <.(F \/ H).) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r where r is Element of L : ex p, q being Element of L st ( p "/\" q [= r & p in F & q in H ) } or x in <.(F \/ H).) ) assume x in { r1 where r1 is Element of L : ex p, q being Element of L st ( p "/\" q [= r1 & p in F & q in H ) } ; ::_thesis: x in <.(F \/ H).) then consider r being Element of L such that A14: x = r and A15: ex p, q being Element of L st ( p "/\" q [= r & p in F & q in H ) ; A16: F \/ H c= <.(F \/ H).) by Def4; H c= F \/ H by XBOOLE_1:7; then A17: H c= <.(F \/ H).) by A16, XBOOLE_1:1; consider p, q being Element of L such that A18: p "/\" q [= r and A19: ( p in F & q in H ) by A15; F c= F \/ H by XBOOLE_1:7; then F c= <.(F \/ H).) by A16, XBOOLE_1:1; then p "/\" q in <.(F \/ H).) by A19, A17, Th8; hence x in <.(F \/ H).) by A14, A18, Th9; ::_thesis: verum end; theorem Th36: :: FILTER_0:36 for L being Lattice for F, H being Filter of L holds ( F c= F "/\" H & H c= F "/\" H ) proof let L be Lattice; ::_thesis: for F, H being Filter of L holds ( F c= F "/\" H & H c= F "/\" H ) let F, H be Filter of L; ::_thesis: ( F c= F "/\" H & H c= F "/\" H ) A1: now__::_thesis:_for_F,_H_being_Filter_of_L_holds_F_c=_F_"/\"_H let F, H be Filter of L; ::_thesis: F c= F "/\" H thus F c= F "/\" H ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in F "/\" H ) assume A2: x in F ; ::_thesis: x in F "/\" H then reconsider i = x as Element of L ; consider p being Element of L such that A3: p in H by SUBSET_1:4; i [= i "\/" p by LATTICES:5; then A4: i "/\" (i "\/" p) = i by LATTICES:4; p [= p "\/" i by LATTICES:5; then i "\/" p in H by A3, Th9; hence x in F "/\" H by A2, A4; ::_thesis: verum end; end; F "/\" H = H "/\" F by Th33; hence ( F c= F "/\" H & H c= F "/\" H ) by A1; ::_thesis: verum end; theorem Th37: :: FILTER_0:37 for L being Lattice for F, H being Filter of L holds <.(F \/ H).) = <.(F "/\" H).) proof let L be Lattice; ::_thesis: for F, H being Filter of L holds <.(F \/ H).) = <.(F "/\" H).) let F, H be Filter of L; ::_thesis: <.(F \/ H).) = <.(F "/\" H).) ( F c= F "/\" H & H c= F "/\" H ) by Th36; then F \/ H c= F "/\" H by XBOOLE_1:8; hence <.(F \/ H).) c= <.(F "/\" H).) by Th22; :: according to XBOOLE_0:def_10 ::_thesis: <.(F "/\" H).) c= <.(F \/ H).) F "/\" H c= <.(F \/ H).) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F "/\" H or x in <.(F \/ H).) ) assume x in F "/\" H ; ::_thesis: x in <.(F \/ H).) then consider p, q being Element of L such that A1: x = p "/\" q and A2: p in F and A3: q in H ; H c= F \/ H by XBOOLE_1:7; then A4: q in F \/ H by A3; A5: F \/ H c= <.(F \/ H).) by Def4; F c= F \/ H by XBOOLE_1:7; then p in F \/ H by A2; hence x in <.(F \/ H).) by A1, A4, A5, Th9; ::_thesis: verum end; then <.(F "/\" H).) c= <.<.(F \/ H).).) by Th22; hence <.(F "/\" H).) c= <.(F \/ H).) by Th21; ::_thesis: verum end; theorem Th38: :: FILTER_0:38 for I being I_Lattice for F1, F2 being Filter of I holds <.(F1 \/ F2).) = F1 "/\" F2 proof let I be I_Lattice; ::_thesis: for F1, F2 being Filter of I holds <.(F1 \/ F2).) = F1 "/\" F2 let F1, F2 be Filter of I; ::_thesis: <.(F1 \/ F2).) = F1 "/\" F2 F1 "/\" F2 = <.(F1 "/\" F2).) by Th21; hence <.(F1 \/ F2).) = F1 "/\" F2 by Th37; ::_thesis: verum end; theorem :: FILTER_0:39 for B being B_Lattice for FB, HB being Filter of B holds <.(FB \/ HB).) = FB "/\" HB proof let B be B_Lattice; ::_thesis: for FB, HB being Filter of B holds <.(FB \/ HB).) = FB "/\" HB let FB, HB be Filter of B; ::_thesis: <.(FB \/ HB).) = FB "/\" HB FB "/\" HB = <.(FB "/\" HB).) by Th21; hence <.(FB \/ HB).) = FB "/\" HB by Th37; ::_thesis: verum end; theorem Th40: :: FILTER_0:40 for I being I_Lattice for j, i being Element of I for DI being non empty Subset of I st j in <.(DI \/ {i}).) holds i => j in <.DI.) proof let I be I_Lattice; ::_thesis: for j, i being Element of I for DI being non empty Subset of I st j in <.(DI \/ {i}).) holds i => j in <.DI.) let j, i be Element of I; ::_thesis: for DI being non empty Subset of I st j in <.(DI \/ {i}).) holds i => j in <.DI.) let DI be non empty Subset of I; ::_thesis: ( j in <.(DI \/ {i}).) implies i => j in <.DI.) ) assume A1: j in <.(DI \/ {i}).) ; ::_thesis: i => j in <.DI.) <.(DI \/ {i}).) = <.(<.DI.) \/ {i}).) by Th34 .= <.(<.DI.) \/ <.{i}.)).) by Th34 .= <.(<.DI.) \/ <.i.)).) by Th24 .= <.DI.) "/\" <.i.) by Th38 ; then consider i1, i2 being Element of I such that A2: j = i1 "/\" i2 and A3: i1 in <.DI.) and A4: i2 in <.i.) by A1; i [= i2 by A4, Th15; then i1 "/\" i [= i1 "/\" i2 by LATTICES:9; then i1 [= i => j by A2, Def7; hence i => j in <.DI.) by A3, Th9; ::_thesis: verum end; theorem Th41: :: FILTER_0:41 for I being I_Lattice for i, j, k being Element of I for FI being Filter of I st i => j in FI & j => k in FI holds i => k in FI proof let I be I_Lattice; ::_thesis: for i, j, k being Element of I for FI being Filter of I st i => j in FI & j => k in FI holds i => k in FI let i, j, k be Element of I; ::_thesis: for FI being Filter of I st i => j in FI & j => k in FI holds i => k in FI let FI be Filter of I; ::_thesis: ( i => j in FI & j => k in FI implies i => k in FI ) assume that A1: i => j in FI and A2: j => k in FI ; ::_thesis: i => k in FI A3: FI \/ {i} c= <.(FI \/ {i}).) by Def4; {i} c= FI \/ {i} by XBOOLE_1:7; then A4: {i} c= <.(FI \/ {i}).) by A3, XBOOLE_1:1; FI c= FI \/ {i} by XBOOLE_1:7; then A5: FI c= <.(FI \/ {i}).) by A3, XBOOLE_1:1; i in {i} by TARSKI:def_1; then j in <.(FI \/ {i}).) by A1, A5, A4, Th29; then A6: k in <.(FI \/ {i}).) by A2, A5, Th29; <.FI.) = FI by Th21; hence i => k in FI by A6, Th40; ::_thesis: verum end; theorem Th42: :: FILTER_0:42 for B being B_Lattice for a, b being Element of B holds a => b = (a `) "\/" b proof let B be B_Lattice; ::_thesis: for a, b being Element of B holds a => b = (a `) "\/" b let a, b be Element of B; ::_thesis: a => b = (a `) "\/" b ( a "/\" ((a `) "\/" b) [= b & ( for c being Element of B st a "/\" c [= b holds c [= (a `) "\/" b ) ) by Th27; hence a => b = (a `) "\/" b by Def7; ::_thesis: verum end; theorem Th43: :: FILTER_0:43 for B being B_Lattice for a, b being Element of B holds ( a [= b iff a "/\" (b `) = Bottom B ) proof let B be B_Lattice; ::_thesis: for a, b being Element of B holds ( a [= b iff a "/\" (b `) = Bottom B ) let a, b be Element of B; ::_thesis: ( a [= b iff a "/\" (b `) = Bottom B ) reconsider B9 = B as 0_Lattice ; reconsider B99 = B as 1_Lattice ; reconsider D = B as D_Lattice ; reconsider a9 = a, b9 = b, c9 = a "/\" (b `) as Element of B9 ; reconsider a99 = a, b99 = b as Element of B99 ; reconsider a1 = a, b1 = b as Element of D ; thus ( a [= b implies a "/\" (b `) = Bottom B ) ::_thesis: ( a "/\" (b `) = Bottom B implies a [= b ) proof assume a [= b ; ::_thesis: a "/\" (b `) = Bottom B then a = a "/\" b by LATTICES:4; hence a "/\" (b `) = a "/\" (b "/\" (b `)) by LATTICES:def_7 .= a9 "/\" (Bottom B9) by LATTICES:20 .= Bottom B ; ::_thesis: verum end; assume a "/\" (b `) = Bottom B ; ::_thesis: a [= b then b = b9 "\/" c9 by LATTICES:14 .= (b1 "\/" a1) "/\" (b1 "\/" (b1 `)) by LATTICES:11 .= (b99 "\/" a99) "/\" (Top B99) by LATTICES:21 .= a "\/" b ; hence a [= b by LATTICES:def_3; ::_thesis: verum end; theorem Th44: :: FILTER_0:44 for B being B_Lattice for FB being Filter of B holds ( FB is being_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds ( a in FB or a ` in FB ) ) ) ) proof let B be B_Lattice; ::_thesis: for FB being Filter of B holds ( FB is being_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds ( a in FB or a ` in FB ) ) ) ) let FB be Filter of B; ::_thesis: ( FB is being_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds ( a in FB or a ` in FB ) ) ) ) thus ( FB is being_ultrafilter implies ( FB <> the carrier of B & ( for a being Element of B holds ( a in FB or a ` in FB ) ) ) ) ::_thesis: ( FB <> the carrier of B & ( for a being Element of B holds ( a in FB or a ` in FB ) ) implies FB is being_ultrafilter ) proof reconsider I = B as I_Lattice ; assume that A1: FB <> the carrier of B and A2: for HB being Filter of B st FB c= HB & HB <> the carrier of B holds FB = HB ; :: according to FILTER_0:def_3 ::_thesis: ( FB <> the carrier of B & ( for a being Element of B holds ( a in FB or a ` in FB ) ) ) thus FB <> the carrier of B by A1; ::_thesis: for a being Element of B holds ( a in FB or a ` in FB ) let a be Element of B; ::_thesis: ( a in FB or a ` in FB ) assume A3: not a in FB ; ::_thesis: a ` in FB A4: a in <.a.) ; A5: FB \/ <.a.) c= <.(FB \/ <.a.)).) by Def4; <.a.) c= FB \/ <.a.) by XBOOLE_1:7; then <.a.) c= <.(FB \/ <.a.)).) by A5, XBOOLE_1:1; then ( FB c= FB \/ <.a.) & FB <> <.(FB \/ <.a.)).) ) by A3, A4, XBOOLE_1:7; then <.(FB \/ <.a.)).) = the carrier of B by A2, A5, XBOOLE_1:1; then A6: a ` in <.(FB \/ <.a.)).) ; reconsider a9 = a as Element of I ; reconsider FI = FB as Filter of I ; A7: a => (a `) = (a `) "\/" (a `) by Th42; <.{a}.) = <.a.) by Th24; then A8: a9 ` in <.(FI \/ {a9}).) by A6, Th34; FB = <.FB.) by Th21; then a => (a `) in FB by A8, Th40; hence a ` in FB by A7; ::_thesis: verum end; assume that A9: FB <> the carrier of B and A10: for a being Element of B holds ( a in FB or a ` in FB ) ; ::_thesis: FB is being_ultrafilter thus FB <> the carrier of B by A9; :: according to FILTER_0:def_3 ::_thesis: for H being Filter of B st FB c= H & H <> the carrier of B holds FB = H let HB be Filter of B; ::_thesis: ( FB c= HB & HB <> the carrier of B implies FB = HB ) assume that A11: FB c= HB and A12: HB <> the carrier of B and A13: FB <> HB ; ::_thesis: contradiction not for x being set holds ( x in FB iff x in HB ) by A13, TARSKI:1; then consider x being set such that A14: x in HB and A15: not x in FB by A11; reconsider x = x as Element of HB by A14; x ` in FB by A10, A15; then (x `) "/\" x in HB by A11, Th8; then A16: Bottom B in HB by LATTICES:20; HB = <.HB.) by Th21; hence contradiction by A12, A16, Th25; ::_thesis: verum end; theorem :: FILTER_0:45 for B being B_Lattice for FB being Filter of B holds ( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter ) proof let B be B_Lattice; ::_thesis: for FB being Filter of B holds ( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter ) let FB be Filter of B; ::_thesis: ( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter ) thus ( FB <> <.B.) & FB is prime implies FB is being_ultrafilter ) ::_thesis: ( FB is being_ultrafilter implies ( FB <> <.B.) & FB is prime ) ) proof assume that A1: FB <> <.B.) and A2: for a, b being Element of B holds ( a "\/" b in FB iff ( a in FB or b in FB ) ) ; :: according to FILTER_0:def_5 ::_thesis: FB is being_ultrafilter now__::_thesis:_for_a_being_Element_of_B_st_not_a_in_FB_holds_ a_`_in_FB let a be Element of B; ::_thesis: ( not a in FB implies a ` in FB ) assume A3: not a in FB ; ::_thesis: a ` in FB a "\/" (a `) = Top B by LATTICES:21; then a "\/" (a `) in FB by Th11; hence a ` in FB by A2, A3; ::_thesis: verum end; hence FB is being_ultrafilter by A1, Th44; ::_thesis: verum end; assume A4: FB is being_ultrafilter ; ::_thesis: ( FB <> <.B.) & FB is prime ) hence FB <> <.B.) by Th44; ::_thesis: FB is prime let a be Element of B; :: according to FILTER_0:def_5 ::_thesis: for q being Element of B holds ( a "\/" q in FB iff ( a in FB or q in FB ) ) let b be Element of B; ::_thesis: ( a "\/" b in FB iff ( a in FB or b in FB ) ) A5: FB <> the carrier of B by A4, Th44; thus ( not a "\/" b in FB or a in FB or b in FB ) ::_thesis: ( ( a in FB or b in FB ) implies a "\/" b in FB ) proof assume that A6: a "\/" b in FB and A7: ( not a in FB & not b in FB ) ; ::_thesis: contradiction ( a ` in FB & b ` in FB ) by A4, A7, Th44; then (a `) "/\" (b `) in FB by Th8; then (a "\/" b) ` in FB by LATTICES:24; then (a "\/" b) "/\" ((a "\/" b) `) in FB by A6, Th8; then A8: Bottom B in FB by LATTICES:20; FB = <.FB.) by Th21; hence contradiction by A5, A8, Th25; ::_thesis: verum end; thus ( ( a in FB or b in FB ) implies a "\/" b in FB ) by Th10; ::_thesis: verum end; theorem Th46: :: FILTER_0:46 for B being B_Lattice for FB being Filter of B st FB is being_ultrafilter holds for a being Element of B holds ( a in FB iff not a ` in FB ) proof let B be B_Lattice; ::_thesis: for FB being Filter of B st FB is being_ultrafilter holds for a being Element of B holds ( a in FB iff not a ` in FB ) let FB be Filter of B; ::_thesis: ( FB is being_ultrafilter implies for a being Element of B holds ( a in FB iff not a ` in FB ) ) assume A1: FB is being_ultrafilter ; ::_thesis: for a being Element of B holds ( a in FB iff not a ` in FB ) let a be Element of B; ::_thesis: ( a in FB iff not a ` in FB ) thus ( a in FB implies not a ` in FB ) ::_thesis: ( not a ` in FB implies a in FB ) proof assume ( a in FB & a ` in FB ) ; ::_thesis: contradiction then a "/\" (a `) in FB by Th8; then Bottom B in FB by LATTICES:20; then FB = the carrier of B by Th26; hence contradiction by A1, Def3; ::_thesis: verum end; thus ( not a ` in FB implies a in FB ) by A1, Th44; ::_thesis: verum end; theorem :: FILTER_0:47 for B being B_Lattice for a, b being Element of B st a <> b holds ex FB being Filter of B st ( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) ) proof let B be B_Lattice; ::_thesis: for a, b being Element of B st a <> b holds ex FB being Filter of B st ( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) ) let a, b be Element of B; ::_thesis: ( a <> b implies ex FB being Filter of B st ( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) ) ) assume a <> b ; ::_thesis: ex FB being Filter of B st ( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) ) then ( not a [= b or not b [= a ) by LATTICES:8; then ( a "/\" (b `) <> Bottom B or b "/\" (a `) <> Bottom B ) by Th43; then ( ex FB being Filter of B st ( a "/\" (b `) in FB & FB is being_ultrafilter ) or ex FB being Filter of B st ( b "/\" (a `) in FB & FB is being_ultrafilter ) ) by Th20; then consider FB being Filter of B such that A1: FB is being_ultrafilter and A2: ( a "/\" (b `) in FB or b "/\" (a `) in FB ) ; take FB ; ::_thesis: ( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) ) thus FB is being_ultrafilter by A1; ::_thesis: ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) ( ( a in FB & b ` in FB ) or ( b in FB & a ` in FB ) ) by A2, Th8; hence ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) by A1, Th46; ::_thesis: verum end; definition let L be Lattice; let F be Filter of L; func latt F -> Lattice means :Def9: :: FILTER_0:def 9 ex o1, o2 being BinOp of F st ( o1 = the L_join of L || F & o2 = the L_meet of L || F & it = LattStr(# F,o1,o2 #) ); uniqueness for b1, b2 being Lattice st ex o1, o2 being BinOp of F st ( o1 = the L_join of L || F & o2 = the L_meet of L || F & b1 = LattStr(# F,o1,o2 #) ) & ex o1, o2 being BinOp of F st ( o1 = the L_join of L || F & o2 = the L_meet of L || F & b2 = LattStr(# F,o1,o2 #) ) holds b1 = b2 ; existence ex b1 being Lattice ex o1, o2 being BinOp of F st ( o1 = the L_join of L || F & o2 = the L_meet of L || F & b1 = LattStr(# F,o1,o2 #) ) proof reconsider o1 = the L_join of L || F, o2 = the L_meet of L || F as Function of [:F,F:], the carrier of L by FUNCT_2:32; A1: dom o1 = [:F,F:] by FUNCT_2:def_1; rng o1 c= F proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng o1 or y in F ) assume y in rng o1 ; ::_thesis: y in F then consider x being set such that A2: x in dom o1 and A3: y = o1 . x by FUNCT_1:def_3; reconsider p = x `1 , q = x `2 as Element of F by A2, MCART_1:10; x = [(x `1),(x `2)] by A2, MCART_1:21; then o1 . x = p "\/" q by A2, FUNCT_1:47; hence y in F by A3, Th10; ::_thesis: verum end; then reconsider o1 = o1 as Function of [:F,F:],F by A1, FUNCT_2:def_1, RELSET_1:4; A4: dom o2 = [:F,F:] by FUNCT_2:def_1; rng o2 c= F proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng o2 or y in F ) assume y in rng o2 ; ::_thesis: y in F then consider x being set such that A5: x in dom o2 and A6: y = o2 . x by FUNCT_1:def_3; reconsider p = x `1 , q = x `2 as Element of F by A5, MCART_1:10; x = [(x `1),(x `2)] by A5, MCART_1:21; then o2 . x = p "/\" q by A5, FUNCT_1:47; hence y in F by A6, Th8; ::_thesis: verum end; then reconsider o2 = o2 as Function of [:F,F:],F by A4, FUNCT_2:def_1, RELSET_1:4; reconsider K = LattStr(# F,o1,o2 #) as non empty LattStr ; A7: for a, b being Element of K holds ( the L_join of K . (a,b) = the L_join of L . (a,b) & the L_meet of K . (a,b) = the L_meet of L . (a,b) ) proof let a, b be Element of K; ::_thesis: ( the L_join of K . (a,b) = the L_join of L . (a,b) & the L_meet of K . (a,b) = the L_meet of L . (a,b) ) the L_join of K . (a,b) = the L_join of K . [a,b] ; hence ( the L_join of K . (a,b) = the L_join of L . (a,b) & the L_meet of K . (a,b) = the L_meet of L . (a,b) ) by A1, A4, FUNCT_1:47; ::_thesis: verum end; A8: for a, b, c being Element of K holds a "/\" (b "/\" c) = (a "/\" b) "/\" c proof let a, b, c be Element of K; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c reconsider a9 = a, b9 = b, c9 = c as Element of F ; thus a "/\" (b "/\" c) = the L_meet of L . (a,(b "/\" c)) by A7 .= a9 "/\" (b9 "/\" c9) by A7 .= (a9 "/\" b9) "/\" c9 by LATTICES:def_7 .= the L_meet of L . ((a "/\" b),c) by A7 .= (a "/\" b) "/\" c by A7 ; ::_thesis: verum end; A9: for a, b being Element of K holds a "/\" (a "\/" b) = a proof let a, b be Element of K; ::_thesis: a "/\" (a "\/" b) = a reconsider a9 = a, b9 = b as Element of F ; thus a "/\" (a "\/" b) = the L_meet of L . (a,(a "\/" b)) by A7 .= a9 "/\" (a9 "\/" b9) by A7 .= a by LATTICES:def_9 ; ::_thesis: verum end; A10: for a, b being Element of K holds a "/\" b = b "/\" a proof let a, b be Element of K; ::_thesis: a "/\" b = b "/\" a reconsider a9 = a, b9 = b as Element of F ; thus a "/\" b = the L_meet of L . (a9,b9) by A7 .= b9 "/\" a9 by LATTICES:def_2 .= b "/\" a by A7 ; ::_thesis: verum end; A11: for a, b being Element of K holds (a "/\" b) "\/" b = b proof let a, b be Element of K; ::_thesis: (a "/\" b) "\/" b = b reconsider a9 = a, b9 = b as Element of F ; thus (a "/\" b) "\/" b = the L_join of L . ((a "/\" b),b) by A7 .= (a9 "/\" b9) "\/" b9 by A7 .= b by LATTICES:def_8 ; ::_thesis: verum end; A12: for a, b being Element of K holds a "\/" b = b "\/" a proof let a, b be Element of K; ::_thesis: a "\/" b = b "\/" a reconsider a9 = a, b9 = b as Element of F ; thus a "\/" b = the L_join of L . (a9,b9) by A7 .= b9 "\/" a9 by LATTICES:def_1 .= b "\/" a by A7 ; ::_thesis: verum end; for a, b, c being Element of K holds a "\/" (b "\/" c) = (a "\/" b) "\/" c proof let a, b, c be Element of K; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c reconsider a9 = a, b9 = b, c9 = c as Element of F ; thus a "\/" (b "\/" c) = the L_join of L . (a,(b "\/" c)) by A7 .= a9 "\/" (b9 "\/" c9) by A7 .= (a9 "\/" b9) "\/" c9 by LATTICES:def_5 .= the L_join of L . ((a "\/" b),c) by A7 .= (a "\/" b) "\/" c by A7 ; ::_thesis: verum end; then ( K is join-commutative & K is join-associative & K is meet-absorbing & K is meet-commutative & K is meet-associative & K is join-absorbing ) by A12, A11, A10, A8, A9, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; then reconsider Q = K as Lattice ; take Q ; ::_thesis: ex o1, o2 being BinOp of F st ( o1 = the L_join of L || F & o2 = the L_meet of L || F & Q = LattStr(# F,o1,o2 #) ) take o1 ; ::_thesis: ex o2 being BinOp of F st ( o1 = the L_join of L || F & o2 = the L_meet of L || F & Q = LattStr(# F,o1,o2 #) ) take o2 ; ::_thesis: ( o1 = the L_join of L || F & o2 = the L_meet of L || F & Q = LattStr(# F,o1,o2 #) ) thus ( o1 = the L_join of L || F & o2 = the L_meet of L || F & Q = LattStr(# F,o1,o2 #) ) ; ::_thesis: verum end; end; :: deftheorem Def9 defines latt FILTER_0:def_9_:_ for L being Lattice for F being Filter of L for b3 being Lattice holds ( b3 = latt F iff ex o1, o2 being BinOp of F st ( o1 = the L_join of L || F & o2 = the L_meet of L || F & b3 = LattStr(# F,o1,o2 #) ) ); registration let L be Lattice; let F be Filter of L; cluster latt F -> strict ; coherence latt F is strict proof ex o1, o2 being BinOp of F st ( o1 = the L_join of L || F & o2 = the L_meet of L || F & latt F = LattStr(# F,o1,o2 #) ) by Def9; hence latt F is strict ; ::_thesis: verum end; end; theorem :: FILTER_0:48 for L being strict Lattice holds latt <.L.) = L proof let L be strict Lattice; ::_thesis: latt <.L.) = L dom the L_meet of L = [: the carrier of L, the carrier of L:] by FUNCT_2:def_1; then A1: the L_meet of L = the L_meet of L || the carrier of L by RELAT_1:68; dom the L_join of L = [: the carrier of L, the carrier of L:] by FUNCT_2:def_1; then the L_join of L = the L_join of L || the carrier of L by RELAT_1:68; hence latt <.L.) = L by A1, Def9; ::_thesis: verum end; theorem Th49: :: FILTER_0:49 for L being Lattice for F being Filter of L holds ( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F ) proof let L be Lattice; ::_thesis: for F being Filter of L holds ( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F ) let F be Filter of L; ::_thesis: ( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F ) ex o1, o2 being BinOp of F st ( o1 = the L_join of L || F & o2 = the L_meet of L || F & latt F = LattStr(# F,o1,o2 #) ) by Def9; hence ( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F ) ; ::_thesis: verum end; theorem Th50: :: FILTER_0:50 for L being Lattice for p, q being Element of L for F being Filter of L for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) proof let L be Lattice; ::_thesis: for p, q being Element of L for F being Filter of L for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) let p, q be Element of L; ::_thesis: for F being Filter of L for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) let F be Filter of L; ::_thesis: for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) let p9, q9 be Element of (latt F); ::_thesis: ( p = p9 & q = q9 implies ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) ) assume A1: ( p = p9 & q = q9 ) ; ::_thesis: ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) consider o1, o2 being BinOp of F such that A2: o1 = the L_join of L || F and A3: o2 = the L_meet of L || F and A4: latt F = LattStr(# F,o1,o2 #) by Def9; dom o1 = [:F,F:] by FUNCT_2:def_1; then [p,q] in dom o1 by A1, A4, ZFMISC_1:87; hence p "\/" q = p9 "\/" q9 by A1, A2, A4, FUNCT_1:47; ::_thesis: p "/\" q = p9 "/\" q9 dom o2 = [:F,F:] by FUNCT_2:def_1; then [p,q] in dom o2 by A1, A4, ZFMISC_1:87; hence p "/\" q = p9 "/\" q9 by A1, A3, A4, FUNCT_1:47; ::_thesis: verum end; theorem Th51: :: FILTER_0:51 for L being Lattice for p, q being Element of L for F being Filter of L for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds ( p [= q iff p9 [= q9 ) proof let L be Lattice; ::_thesis: for p, q being Element of L for F being Filter of L for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds ( p [= q iff p9 [= q9 ) let p, q be Element of L; ::_thesis: for F being Filter of L for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds ( p [= q iff p9 [= q9 ) let F be Filter of L; ::_thesis: for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds ( p [= q iff p9 [= q9 ) let p9, q9 be Element of (latt F); ::_thesis: ( p = p9 & q = q9 implies ( p [= q iff p9 [= q9 ) ) A1: ( p [= q iff p "\/" q = q ) by LATTICES:def_3; A2: ( p9 [= q9 iff p9 "\/" q9 = q9 ) by LATTICES:def_3; assume ( p = p9 & q = q9 ) ; ::_thesis: ( p [= q iff p9 [= q9 ) hence ( p [= q iff p9 [= q9 ) by A1, A2, Th50; ::_thesis: verum end; theorem Th52: :: FILTER_0:52 for L being Lattice for F being Filter of L st L is upper-bounded holds latt F is upper-bounded proof let L be Lattice; ::_thesis: for F being Filter of L st L is upper-bounded holds latt F is upper-bounded let F be Filter of L; ::_thesis: ( L is upper-bounded implies latt F is upper-bounded ) given p being Element of L such that A1: for q being Element of L holds ( p "\/" q = p & q "\/" p = p ) ; :: according to LATTICES:def_14 ::_thesis: latt F is upper-bounded consider q being Element of L such that A2: q in F by SUBSET_1:4; A3: ex o1, o2 being BinOp of F st ( o1 = the L_join of L || F & o2 = the L_meet of L || F & latt F = LattStr(# F,o1,o2 #) ) by Def9; p "\/" q = p by A1; then reconsider p9 = p as Element of (latt F) by A2, A3, Th10; take p9 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (latt F) holds ( p9 "\/" b1 = p9 & b1 "\/" p9 = p9 ) let r be Element of (latt F); ::_thesis: ( p9 "\/" r = p9 & r "\/" p9 = p9 ) reconsider r9 = r as Element of F by A3; thus p9 "\/" r = p "\/" r9 by Th50 .= p9 by A1 ; ::_thesis: r "\/" p9 = p9 hence r "\/" p9 = p9 ; ::_thesis: verum end; theorem :: FILTER_0:53 for L being Lattice for F being Filter of L st L is modular holds latt F is modular proof let L be Lattice; ::_thesis: for F being Filter of L st L is modular holds latt F is modular let F be Filter of L; ::_thesis: ( L is modular implies latt F is modular ) assume A1: for a, b, c being Element of L st a [= c holds a "\/" (b "/\" c) = (a "\/" b) "/\" c ; :: according to LATTICES:def_12 ::_thesis: latt F is modular let a, b, c be Element of (latt F); :: according to LATTICES:def_12 ::_thesis: ( not a [= c or a "\/" (b "/\" c) = (a "\/" b) "/\" c ) assume A2: a [= c ; ::_thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c reconsider p = a, q = b, r = c as Element of F by Th49; b "/\" c = q "/\" r by Th50; then A3: a "\/" (b "/\" c) = p "\/" (q "/\" r) by Th50; a "\/" b = p "\/" q by Th50; then A4: (a "\/" b) "/\" c = (p "\/" q) "/\" r by Th50; p [= r by A2, Th51; hence a "\/" (b "/\" c) = (a "\/" b) "/\" c by A1, A3, A4; ::_thesis: verum end; theorem Th54: :: FILTER_0:54 for L being Lattice for F being Filter of L st L is distributive holds latt F is distributive proof let L be Lattice; ::_thesis: for F being Filter of L st L is distributive holds latt F is distributive let F be Filter of L; ::_thesis: ( L is distributive implies latt F is distributive ) assume A1: for p, q, r being Element of L holds p "/\" (q "\/" r) = (p "/\" q) "\/" (p "/\" r) ; :: according to LATTICES:def_11 ::_thesis: latt F is distributive let p9, q9, r9 be Element of (latt F); :: according to LATTICES:def_11 ::_thesis: p9 "/\" (q9 "\/" r9) = (p9 "/\" q9) "\/" (p9 "/\" r9) reconsider p = p9, q = q9, r = r9, qr = q9 "\/" r9 as Element of F by Th49; A2: ( p9 "/\" q9 = p "/\" q & p9 "/\" r9 = p "/\" r ) by Th50; thus p9 "/\" (q9 "\/" r9) = p "/\" qr by Th50 .= p "/\" (q "\/" r) by Th50 .= (p "/\" q) "\/" (p "/\" r) by A1 .= (p9 "/\" q9) "\/" (p9 "/\" r9) by A2, Th50 ; ::_thesis: verum end; theorem :: FILTER_0:55 for L being Lattice for F being Filter of L st L is I_Lattice holds latt F is implicative proof let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds latt F is implicative let F be Filter of L; ::_thesis: ( L is I_Lattice implies latt F is implicative ) assume A1: L is I_Lattice ; ::_thesis: latt F is implicative then reconsider I = L as I_Lattice ; reconsider FI = F as Filter of I ; let p9, q9 be Element of (latt F); :: according to FILTER_0:def_6 ::_thesis: ex r being Element of (latt F) st ( p9 "/\" r [= q9 & ( for r1 being Element of (latt F) st p9 "/\" r1 [= q9 holds r1 [= r ) ) reconsider p = p9, q = q9 as Element of F by Th49; consider r being Element of L such that A2: p "/\" r [= q and A3: for r1 being Element of L st p "/\" r1 [= q holds r1 [= r by A1, Def6; reconsider i = p, j = q as Element of I ; A4: i => j in FI by Th30; i => j = r by A2, A3, Def7; then reconsider r9 = r as Element of (latt F) by A4, Th49; take r9 ; ::_thesis: ( p9 "/\" r9 [= q9 & ( for r1 being Element of (latt F) st p9 "/\" r1 [= q9 holds r1 [= r9 ) ) p "/\" r = p9 "/\" r9 by Th50; hence p9 "/\" r9 [= q9 by A2, Th51; ::_thesis: for r1 being Element of (latt F) st p9 "/\" r1 [= q9 holds r1 [= r9 let s9 be Element of (latt F); ::_thesis: ( p9 "/\" s9 [= q9 implies s9 [= r9 ) assume A5: p9 "/\" s9 [= q9 ; ::_thesis: s9 [= r9 reconsider s = s9 as Element of F by Th49; p "/\" s = p9 "/\" s9 by Th50; then p "/\" s [= q by A5, Th51; then s [= r by A3; hence s9 [= r9 by Th51; ::_thesis: verum end; registration let L be Lattice; let p be Element of L; cluster latt <.p.) -> lower-bounded ; coherence latt <.p.) is lower-bounded proof the carrier of (latt <.p.)) = <.p.) by Th49; then reconsider p9 = p as Element of (latt <.p.)) by Th16; take p9 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (latt <.p.)) holds ( p9 "/\" b1 = p9 & b1 "/\" p9 = p9 ) let q9 be Element of (latt <.p.)); ::_thesis: ( p9 "/\" q9 = p9 & q9 "/\" p9 = p9 ) reconsider q = q9 as Element of <.p.) by Th49; p [= q by Th15; then p "/\" q = p by LATTICES:4; hence ( p9 "/\" q9 = p9 & q9 "/\" p9 = p9 ) by Th50; ::_thesis: verum end; end; theorem Th56: :: FILTER_0:56 for L being Lattice for p being Element of L holds Bottom (latt <.p.)) = p proof let L be Lattice; ::_thesis: for p being Element of L holds Bottom (latt <.p.)) = p let p be Element of L; ::_thesis: Bottom (latt <.p.)) = p consider q9 being Element of (latt <.p.)) such that A1: for r9 being Element of (latt <.p.)) holds ( q9 "/\" r9 = q9 & r9 "/\" q9 = q9 ) by LATTICES:def_13; the carrier of (latt <.p.)) = <.p.) by Th49; then reconsider p9 = p as Element of (latt <.p.)) by Th16; reconsider q = q9 as Element of <.p.) by Th49; q9 "/\" p9 = q9 by A1; then q9 [= p9 by LATTICES:4; then A2: q [= p by Th51; A3: p [= q by Th15; q9 = Bottom (latt <.p.)) by A1, RLSUB_2:64; hence Bottom (latt <.p.)) = p by A2, A3, LATTICES:8; ::_thesis: verum end; theorem Th57: :: FILTER_0:57 for L being Lattice for p being Element of L st L is upper-bounded holds Top (latt <.p.)) = Top L proof let L be Lattice; ::_thesis: for p being Element of L st L is upper-bounded holds Top (latt <.p.)) = Top L let p be Element of L; ::_thesis: ( L is upper-bounded implies Top (latt <.p.)) = Top L ) given q being Element of L such that A1: for r being Element of L holds ( q "\/" r = q & r "\/" q = q ) ; :: according to LATTICES:def_14 ::_thesis: Top (latt <.p.)) = Top L L is 1_Lattice by A1, LATTICES:def_14; then Top L in <.p.) by Th11; then reconsider q9 = Top L as Element of (latt <.p.)) by Th49; A2: q = Top L by A1, RLSUB_2:65; now__::_thesis:_for_r9_being_Element_of_(latt_<.p.))_holds_r9_"\/"_q9_=_q9 let r9 be Element of (latt <.p.)); ::_thesis: r9 "\/" q9 = q9 reconsider r = r9 as Element of <.p.) by Th49; thus r9 "\/" q9 = q "\/" r by A2, Th50 .= q9 by A1, A2 ; ::_thesis: verum end; hence Top (latt <.p.)) = Top L by RLSUB_2:65; ::_thesis: verum end; theorem Th58: :: FILTER_0:58 for L being Lattice for p being Element of L st L is 1_Lattice holds latt <.p.) is bounded proof let L be Lattice; ::_thesis: for p being Element of L st L is 1_Lattice holds latt <.p.) is bounded let p be Element of L; ::_thesis: ( L is 1_Lattice implies latt <.p.) is bounded ) assume L is 1_Lattice ; ::_thesis: latt <.p.) is bounded hence ( latt <.p.) is lower-bounded & latt <.p.) is upper-bounded ) by Th52; :: according to LATTICES:def_15 ::_thesis: verum end; theorem Th59: :: FILTER_0:59 for L being Lattice for p being Element of L st L is C_Lattice & L is M_Lattice holds latt <.p.) is C_Lattice proof let L be Lattice; ::_thesis: for p being Element of L st L is C_Lattice & L is M_Lattice holds latt <.p.) is C_Lattice let p be Element of L; ::_thesis: ( L is C_Lattice & L is M_Lattice implies latt <.p.) is C_Lattice ) assume that A1: L is C_Lattice and A2: L is M_Lattice ; ::_thesis: latt <.p.) is C_Lattice reconsider B = L as C_Lattice by A1; reconsider M = latt <.p.) as 01_Lattice by A1, Th58; M is complemented proof let r9 be Element of M; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of M st b1 is_a_complement_of r9 reconsider r = r9 as Element of <.p.) by Th49; reconsider p1 = p as Element of B ; consider q being Element of L such that A3: q is_a_complement_of r by A1, LATTICES:def_19; the carrier of (latt <.p.)) = <.p.) by Th49; then reconsider q9 = p "\/" q as Element of M by Th16; take q9 ; ::_thesis: q9 is_a_complement_of r9 thus q9 "\/" r9 = (p "\/" q) "\/" r by Th50 .= p "\/" (q "\/" r) by LATTICES:def_5 .= p1 "\/" (Top B) by A3, LATTICES:def_18 .= Top L .= Top M by A1, Th57 ; :: according to LATTICES:def_18 ::_thesis: ( r9 "\/" q9 = Top M & q9 "/\" r9 = Bottom M & r9 "/\" q9 = Bottom M ) hence r9 "\/" q9 = Top M ; ::_thesis: ( q9 "/\" r9 = Bottom M & r9 "/\" q9 = Bottom M ) p [= r by Th15; then (p "\/" q) "/\" r = p "\/" (q "/\" r) by A2, LATTICES:def_12; hence q9 "/\" r9 = p "\/" (q "/\" r) by Th50 .= p1 "\/" (Bottom B) by A3, LATTICES:def_18 .= p .= Bottom M by Th56 ; ::_thesis: r9 "/\" q9 = Bottom M hence r9 "/\" q9 = Bottom M ; ::_thesis: verum end; hence latt <.p.) is C_Lattice ; ::_thesis: verum end; theorem :: FILTER_0:60 for L being Lattice for p being Element of L st L is B_Lattice holds latt <.p.) is B_Lattice proof let L be Lattice; ::_thesis: for p being Element of L st L is B_Lattice holds latt <.p.) is B_Lattice let p be Element of L; ::_thesis: ( L is B_Lattice implies latt <.p.) is B_Lattice ) assume L is B_Lattice ; ::_thesis: latt <.p.) is B_Lattice then latt <.p.) is distributive bounded complemented Lattice by Th54, Th59; hence latt <.p.) is B_Lattice ; ::_thesis: verum end; definition let L be Lattice; let p, q be Element of L; funcp <=> q -> Element of L equals :: FILTER_0:def 10 (p => q) "/\" (q => p); correctness coherence (p => q) "/\" (q => p) is Element of L; ; end; :: deftheorem defines <=> FILTER_0:def_10_:_ for L being Lattice for p, q being Element of L holds p <=> q = (p => q) "/\" (q => p); theorem :: FILTER_0:61 for L being Lattice for p, q being Element of L holds p <=> q = q <=> p ; theorem Th62: :: FILTER_0:62 for I being I_Lattice for i, j, k being Element of I for FI being Filter of I st i <=> j in FI & j <=> k in FI holds i <=> k in FI proof let I be I_Lattice; ::_thesis: for i, j, k being Element of I for FI being Filter of I st i <=> j in FI & j <=> k in FI holds i <=> k in FI let i, j, k be Element of I; ::_thesis: for FI being Filter of I st i <=> j in FI & j <=> k in FI holds i <=> k in FI let FI be Filter of I; ::_thesis: ( i <=> j in FI & j <=> k in FI implies i <=> k in FI ) assume A1: ( i <=> j in FI & j <=> k in FI ) ; ::_thesis: i <=> k in FI then ( j => i in FI & k => j in FI ) by Th8; then A2: k => i in FI by Th41; ( i => j in FI & j => k in FI ) by A1, Th8; then i => k in FI by Th41; hence i <=> k in FI by A2, Th8; ::_thesis: verum end; definition let L be Lattice; let F be Filter of L; func equivalence_wrt F -> Relation means :Def11: :: FILTER_0:def 11 ( field it c= the carrier of L & ( for p, q being Element of L holds ( [p,q] in it iff p <=> q in F ) ) ); existence ex b1 being Relation st ( field b1 c= the carrier of L & ( for p, q being Element of L holds ( [p,q] in b1 iff p <=> q in F ) ) ) proof defpred S1[ set , set ] means ex p, q being Element of L st ( \$1 = p & \$2 = q & p <=> q in F ); consider R being Relation such that A1: for x, y being set holds ( [x,y] in R iff ( x in the carrier of L & y in the carrier of L & S1[x,y] ) ) from RELAT_1:sch_1(); take R ; ::_thesis: ( field R c= the carrier of L & ( for p, q being Element of L holds ( [p,q] in R iff p <=> q in F ) ) ) thus field R c= the carrier of L ::_thesis: for p, q being Element of L holds ( [p,q] in R iff p <=> q in F ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in field R or x in the carrier of L ) assume x in field R ; ::_thesis: x in the carrier of L then ex y being set st ( [x,y] in R or [y,x] in R ) by WELLSET1:1; hence x in the carrier of L by A1; ::_thesis: verum end; let p, q be Element of L; ::_thesis: ( [p,q] in R iff p <=> q in F ) thus ( [p,q] in R implies p <=> q in F ) ::_thesis: ( p <=> q in F implies [p,q] in R ) proof assume [p,q] in R ; ::_thesis: p <=> q in F then ex p1, q1 being Element of L st ( p = p1 & q = q1 & p1 <=> q1 in F ) by A1; hence p <=> q in F ; ::_thesis: verum end; thus ( p <=> q in F implies [p,q] in R ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Relation st field b1 c= the carrier of L & ( for p, q being Element of L holds ( [p,q] in b1 iff p <=> q in F ) ) & field b2 c= the carrier of L & ( for p, q being Element of L holds ( [p,q] in b2 iff p <=> q in F ) ) holds b1 = b2 proof let R1, R2 be Relation; ::_thesis: ( field R1 c= the carrier of L & ( for p, q being Element of L holds ( [p,q] in R1 iff p <=> q in F ) ) & field R2 c= the carrier of L & ( for p, q being Element of L holds ( [p,q] in R2 iff p <=> q in F ) ) implies R1 = R2 ) assume that A2: field R1 c= the carrier of L and A3: for p, q being Element of L holds ( [p,q] in R1 iff p <=> q in F ) and A4: field R2 c= the carrier of L and A5: for p, q being Element of L holds ( [p,q] in R2 iff p <=> q in F ) ; ::_thesis: R1 = R2 let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds ( ( not [x,b1] in R1 or [x,b1] in R2 ) & ( not [x,b1] in R2 or [x,b1] in R1 ) ) let y be set ; ::_thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) ) thus ( [x,y] in R1 implies [x,y] in R2 ) ::_thesis: ( not [x,y] in R2 or [x,y] in R1 ) proof assume A6: [x,y] in R1 ; ::_thesis: [x,y] in R2 then ( x in field R1 & y in field R1 ) by RELAT_1:15; then reconsider p = x, q = y as Element of L by A2; p <=> q in F by A3, A6; hence [x,y] in R2 by A5; ::_thesis: verum end; assume A7: [x,y] in R2 ; ::_thesis: [x,y] in R1 then ( x in field R2 & y in field R2 ) by RELAT_1:15; then reconsider p = x, q = y as Element of L by A4; p <=> q in F by A5, A7; hence [x,y] in R1 by A3; ::_thesis: verum end; end; :: deftheorem Def11 defines equivalence_wrt FILTER_0:def_11_:_ for L being Lattice for F being Filter of L for b3 being Relation holds ( b3 = equivalence_wrt F iff ( field b3 c= the carrier of L & ( for p, q being Element of L holds ( [p,q] in b3 iff p <=> q in F ) ) ) ); theorem Th63: :: FILTER_0:63 for L being Lattice for F being Filter of L holds equivalence_wrt F is Relation of the carrier of L proof let L be Lattice; ::_thesis: for F being Filter of L holds equivalence_wrt F is Relation of the carrier of L let F be Filter of L; ::_thesis: equivalence_wrt F is Relation of the carrier of L equivalence_wrt F c= [: the carrier of L, the carrier of L:] proof let y be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds ( not [y,b1] in equivalence_wrt F or [y,b1] in [: the carrier of L, the carrier of L:] ) let z be set ; ::_thesis: ( not [y,z] in equivalence_wrt F or [y,z] in [: the carrier of L, the carrier of L:] ) assume [y,z] in equivalence_wrt F ; ::_thesis: [y,z] in [: the carrier of L, the carrier of L:] then A1: ( y in field (equivalence_wrt F) & z in field (equivalence_wrt F) ) by RELAT_1:15; field (equivalence_wrt F) c= the carrier of L by Def11; hence [y,z] in [: the carrier of L, the carrier of L:] by A1, ZFMISC_1:87; ::_thesis: verum end; hence equivalence_wrt F is Relation of the carrier of L ; ::_thesis: verum end; theorem Th64: :: FILTER_0:64 for L being Lattice for F being Filter of L st L is I_Lattice holds equivalence_wrt F is_reflexive_in the carrier of L proof let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds equivalence_wrt F is_reflexive_in the carrier of L let F be Filter of L; ::_thesis: ( L is I_Lattice implies equivalence_wrt F is_reflexive_in the carrier of L ) assume A1: L is I_Lattice ; ::_thesis: equivalence_wrt F is_reflexive_in the carrier of L let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in the carrier of L or [x,x] in equivalence_wrt F ) assume x in the carrier of L ; ::_thesis: [x,x] in equivalence_wrt F then reconsider p = x as Element of L ; p => p = Top L by A1, Th28; then p <=> p = Top L ; then p <=> p in F by A1, Th11; hence [x,x] in equivalence_wrt F by Def11; ::_thesis: verum end; theorem Th65: :: FILTER_0:65 for L being Lattice for F being Filter of L holds equivalence_wrt F is_symmetric_in the carrier of L proof let L be Lattice; ::_thesis: for F being Filter of L holds equivalence_wrt F is_symmetric_in the carrier of L let F be Filter of L; ::_thesis: equivalence_wrt F is_symmetric_in the carrier of L let x be set ; :: according to RELAT_2:def_3 ::_thesis: for b1 being set holds ( not x in the carrier of L or not b1 in the carrier of L or not [x,b1] in equivalence_wrt F or [b1,x] in equivalence_wrt F ) let y be set ; ::_thesis: ( not x in the carrier of L or not y in the carrier of L or not [x,y] in equivalence_wrt F or [y,x] in equivalence_wrt F ) assume ( x in the carrier of L & y in the carrier of L ) ; ::_thesis: ( not [x,y] in equivalence_wrt F or [y,x] in equivalence_wrt F ) then reconsider p = x, q = y as Element of L ; assume [x,y] in equivalence_wrt F ; ::_thesis: [y,x] in equivalence_wrt F then p <=> q in F by Def11; then q <=> p in F ; hence [y,x] in equivalence_wrt F by Def11; ::_thesis: verum end; theorem Th66: :: FILTER_0:66 for L being Lattice for F being Filter of L st L is I_Lattice holds equivalence_wrt F is_transitive_in the carrier of L proof let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds equivalence_wrt F is_transitive_in the carrier of L let F be Filter of L; ::_thesis: ( L is I_Lattice implies equivalence_wrt F is_transitive_in the carrier of L ) assume A1: L is I_Lattice ; ::_thesis: equivalence_wrt F is_transitive_in the carrier of L let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds ( not x in the carrier of L or not b1 in the carrier of L or not b2 in the carrier of L or not [x,b1] in equivalence_wrt F or not [b1,b2] in equivalence_wrt F or [x,b2] in equivalence_wrt F ) let y, z be set ; ::_thesis: ( not x in the carrier of L or not y in the carrier of L or not z in the carrier of L or not [x,y] in equivalence_wrt F or not [y,z] in equivalence_wrt F or [x,z] in equivalence_wrt F ) assume ( x in the carrier of L & y in the carrier of L & z in the carrier of L ) ; ::_thesis: ( not [x,y] in equivalence_wrt F or not [y,z] in equivalence_wrt F or [x,z] in equivalence_wrt F ) then reconsider p = x, q = y, r = z as Element of L ; assume ( [x,y] in equivalence_wrt F & [y,z] in equivalence_wrt F ) ; ::_thesis: [x,z] in equivalence_wrt F then ( p <=> q in F & q <=> r in F ) by Def11; then p <=> r in F by A1, Th62; hence [x,z] in equivalence_wrt F by Def11; ::_thesis: verum end; theorem Th67: :: FILTER_0:67 for L being Lattice for F being Filter of L st L is I_Lattice holds equivalence_wrt F is Equivalence_Relation of the carrier of L proof let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds equivalence_wrt F is Equivalence_Relation of the carrier of L let F be Filter of L; ::_thesis: ( L is I_Lattice implies equivalence_wrt F is Equivalence_Relation of the carrier of L ) reconsider R = equivalence_wrt F as Relation of the carrier of L by Th63; A1: R is_symmetric_in the carrier of L by Th65; assume A2: L is I_Lattice ; ::_thesis: equivalence_wrt F is Equivalence_Relation of the carrier of L then R is_reflexive_in the carrier of L by Th64; then A3: ( field R = the carrier of L & dom R = the carrier of L ) by ORDERS_1:13; R is_transitive_in the carrier of L by A2, Th66; hence equivalence_wrt F is Equivalence_Relation of the carrier of L by A3, A1, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum end; theorem :: FILTER_0:68 for L being Lattice for F being Filter of L st L is I_Lattice holds field (equivalence_wrt F) = the carrier of L proof let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds field (equivalence_wrt F) = the carrier of L let F be Filter of L; ::_thesis: ( L is I_Lattice implies field (equivalence_wrt F) = the carrier of L ) assume L is I_Lattice ; ::_thesis: field (equivalence_wrt F) = the carrier of L then equivalence_wrt F is Equivalence_Relation of the carrier of L by Th67; hence field (equivalence_wrt F) = the carrier of L by ORDERS_1:12; ::_thesis: verum end; definition let I be I_Lattice; let FI be Filter of I; :: original: equivalence_wrt redefine func equivalence_wrt FI -> Equivalence_Relation of the carrier of I; coherence equivalence_wrt FI is Equivalence_Relation of the carrier of I by Th67; end; definition let B be B_Lattice; let FB be Filter of B; :: original: equivalence_wrt redefine func equivalence_wrt FB -> Equivalence_Relation of the carrier of B; coherence equivalence_wrt FB is Equivalence_Relation of the carrier of B by Th67; end; definition let L be Lattice; let F be Filter of L; let p, q be Element of L; predp,q are_equivalence_wrt F means :Def12: :: FILTER_0:def 12 p <=> q in F; end; :: deftheorem Def12 defines are_equivalence_wrt FILTER_0:def_12_:_ for L being Lattice for F being Filter of L for p, q being Element of L holds ( p,q are_equivalence_wrt F iff p <=> q in F ); theorem :: FILTER_0:69 for L being Lattice for p, q being Element of L for F being Filter of L holds ( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F ) proof let L be Lattice; ::_thesis: for p, q being Element of L for F being Filter of L holds ( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F ) let p, q be Element of L; ::_thesis: for F being Filter of L holds ( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F ) let F be Filter of L; ::_thesis: ( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F ) ( p,q are_equivalence_wrt F iff p <=> q in F ) by Def12; hence ( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F ) by Def11; ::_thesis: verum end; theorem :: FILTER_0:70 for B being B_Lattice for FB being Filter of B for I being I_Lattice for i being Element of I for FI being Filter of I for a being Element of B holds ( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB ) proof let B be B_Lattice; ::_thesis: for FB being Filter of B for I being I_Lattice for i being Element of I for FI being Filter of I for a being Element of B holds ( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB ) let FB be Filter of B; ::_thesis: for I being I_Lattice for i being Element of I for FI being Filter of I for a being Element of B holds ( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB ) let I be I_Lattice; ::_thesis: for i being Element of I for FI being Filter of I for a being Element of B holds ( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB ) let i be Element of I; ::_thesis: for FI being Filter of I for a being Element of B holds ( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB ) let FI be Filter of I; ::_thesis: for a being Element of B holds ( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB ) let a be Element of B; ::_thesis: ( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB ) A2: a => a = Top B by Th28; ( i => i = Top I & (Top I) "/\" (Top I) = Top I ) by Th28; hence ( i <=> i in FI & a <=> a in FB ) by A2, Th11; :: according to FILTER_0:def_12 ::_thesis: verum end; theorem :: FILTER_0:71 for L being Lattice for p, q being Element of L for F being Filter of L st p,q are_equivalence_wrt F holds q,p are_equivalence_wrt F proof let L be Lattice; ::_thesis: for p, q being Element of L for F being Filter of L st p,q are_equivalence_wrt F holds q,p are_equivalence_wrt F let p, q be Element of L; ::_thesis: for F being Filter of L st p,q are_equivalence_wrt F holds q,p are_equivalence_wrt F let F be Filter of L; ::_thesis: ( p,q are_equivalence_wrt F implies q,p are_equivalence_wrt F ) assume p <=> q in F ; :: according to FILTER_0:def_12 ::_thesis: q,p are_equivalence_wrt F hence q <=> p in F ; :: according to FILTER_0:def_12 ::_thesis: verum end; theorem :: FILTER_0:72 for B being B_Lattice for FB being Filter of B for I being I_Lattice for i, j, k being Element of I for FI being Filter of I for a, b, c being Element of B holds ( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) ) proof let B be B_Lattice; ::_thesis: for FB being Filter of B for I being I_Lattice for i, j, k being Element of I for FI being Filter of I for a, b, c being Element of B holds ( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) ) let FB be Filter of B; ::_thesis: for I being I_Lattice for i, j, k being Element of I for FI being Filter of I for a, b, c being Element of B holds ( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) ) let I be I_Lattice; ::_thesis: for i, j, k being Element of I for FI being Filter of I for a, b, c being Element of B holds ( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) ) let i, j, k be Element of I; ::_thesis: for FI being Filter of I for a, b, c being Element of B holds ( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) ) let FI be Filter of I; ::_thesis: for a, b, c being Element of B holds ( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) ) let a, b, c be Element of B; ::_thesis: ( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) ) thus ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) ::_thesis: ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) proof assume ( i <=> j in FI & j <=> k in FI ) ; :: according to FILTER_0:def_12 ::_thesis: i,k are_equivalence_wrt FI hence i <=> k in FI by Th62; :: according to FILTER_0:def_12 ::_thesis: verum end; assume ( a <=> b in FB & b <=> c in FB ) ; :: according to FILTER_0:def_12 ::_thesis: a,c are_equivalence_wrt FB hence a <=> c in FB by Th62; :: according to FILTER_0:def_12 ::_thesis: verum end; begin theorem :: FILTER_0:73 for L being non empty join-commutative meet-commutative meet-associative meet-absorbing join-absorbing LattStr for x, y, z being Element of L st z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds z9 [= z ) holds z = x "/\" y proof let L be non empty join-commutative meet-commutative meet-associative meet-absorbing join-absorbing LattStr ; ::_thesis: for x, y, z being Element of L st z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds z9 [= z ) holds z = x "/\" y let x, y, z be Element of L; ::_thesis: ( z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds z9 [= z ) implies z = x "/\" y ) assume that A1: ( z [= x & z [= y ) and A2: for z9 being Element of L st z9 [= x & z9 [= y holds z9 [= z ; ::_thesis: z = x "/\" y ( x "/\" y [= x & x "/\" y [= y ) by LATTICES:6; then A3: x "/\" y [= z by A2; z [= x "/\" y by A1, Th7; hence z = x "/\" y by A3, LATTICES:8; ::_thesis: verum end; theorem :: FILTER_0:74 for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr for x, y, z being Element of L st x [= z & y [= z & ( for z9 being Element of L st x [= z9 & y [= z9 holds z [= z9 ) holds z = x "\/" y proof let L be non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr ; ::_thesis: for x, y, z being Element of L st x [= z & y [= z & ( for z9 being Element of L st x [= z9 & y [= z9 holds z [= z9 ) holds z = x "\/" y let x, y, z be Element of L; ::_thesis: ( x [= z & y [= z & ( for z9 being Element of L st x [= z9 & y [= z9 holds z [= z9 ) implies z = x "\/" y ) assume that A1: ( x [= z & y [= z ) and A2: for z9 being Element of L st x [= z9 & y [= z9 holds z [= z9 ; ::_thesis: z = x "\/" y ( x [= x "\/" y & y [= x "\/" y ) by LATTICES:5; then A3: z [= x "\/" y by A2; x "\/" y [= z by A1, Th6; hence z = x "\/" y by A3, LATTICES:8; ::_thesis: verum end;