:: WAYBEL_8 semantic presentation begin definition let L be non empty reflexive RelStr ; func CompactSublatt L -> strict full SubRelStr of L means :Def1: :: WAYBEL_8:def 1 for x being Element of L holds ( x in the carrier of it iff x is compact ); existence ex b1 being strict full SubRelStr of L st for x being Element of L holds ( x in the carrier of b1 iff x is compact ) proof defpred S1[ set ] means ex y being Element of L st ( y = \$1 & y is compact ); consider X being Subset of L such that A1: for x being set holds ( x in X iff ( x in the carrier of L & S1[x] ) ) from SUBSET_1:sch_1(); reconsider S = RelStr(# X,( the InternalRel of L |_2 X) #) as strict full SubRelStr of L by YELLOW_0:56; take S ; ::_thesis: for x being Element of L holds ( x in the carrier of S iff x is compact ) let x be Element of L; ::_thesis: ( x in the carrier of S iff x is compact ) thus ( x in the carrier of S implies x is compact ) ::_thesis: ( x is compact implies x in the carrier of S ) proof assume x in the carrier of S ; ::_thesis: x is compact then ex y being Element of L st ( y = x & y is compact ) by A1; hence x is compact ; ::_thesis: verum end; thus ( x is compact implies x in the carrier of S ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being strict full SubRelStr of L st ( for x being Element of L holds ( x in the carrier of b1 iff x is compact ) ) & ( for x being Element of L holds ( x in the carrier of b2 iff x is compact ) ) holds b1 = b2 proof let K1, K2 be strict full SubRelStr of L; ::_thesis: ( ( for x being Element of L holds ( x in the carrier of K1 iff x is compact ) ) & ( for x being Element of L holds ( x in the carrier of K2 iff x is compact ) ) implies K1 = K2 ) assume that A2: for x being Element of L holds ( x in the carrier of K1 iff x is compact ) and A3: for x being Element of L holds ( x in the carrier of K2 iff x is compact ) ; ::_thesis: K1 = K2 now__::_thesis:_for_x_being_set_holds_ (_(_x_in_the_carrier_of_K1_implies_x_in_the_carrier_of_K2_)_&_(_x_in_the_carrier_of_K2_implies_x_in_the_carrier_of_K1_)_) let x be set ; ::_thesis: ( ( x in the carrier of K1 implies x in the carrier of K2 ) & ( x in the carrier of K2 implies x in the carrier of K1 ) ) thus ( x in the carrier of K1 implies x in the carrier of K2 ) ::_thesis: ( x in the carrier of K2 implies x in the carrier of K1 ) proof assume A4: x in the carrier of K1 ; ::_thesis: x in the carrier of K2 the carrier of K1 c= the carrier of L by YELLOW_0:def_13; then reconsider x9 = x as Element of L by A4; x9 is compact by A2, A4; hence x in the carrier of K2 by A3; ::_thesis: verum end; thus ( x in the carrier of K2 implies x in the carrier of K1 ) ::_thesis: verum proof assume A5: x in the carrier of K2 ; ::_thesis: x in the carrier of K1 the carrier of K2 c= the carrier of L by YELLOW_0:def_13; then reconsider x9 = x as Element of L by A5; x9 is compact by A3, A5; hence x in the carrier of K1 by A2; ::_thesis: verum end; end; then the carrier of K1 = the carrier of K2 by TARSKI:1; hence K1 = K2 by YELLOW_0:57; ::_thesis: verum end; end; :: deftheorem Def1 defines CompactSublatt WAYBEL_8:def_1_:_ for L being non empty reflexive RelStr for b2 being strict full SubRelStr of L holds ( b2 = CompactSublatt L iff for x being Element of L holds ( x in the carrier of b2 iff x is compact ) ); registration let L be non empty reflexive antisymmetric lower-bounded RelStr ; cluster CompactSublatt L -> non empty strict full ; coherence not CompactSublatt L is empty proof Bottom L is compact by WAYBEL_3:15; hence not CompactSublatt L is empty by Def1; ::_thesis: verum end; end; theorem :: WAYBEL_8:1 for L being complete LATTICE for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds x << y proof let L be complete LATTICE; ::_thesis: for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds x << y let x, y, k be Element of L; ::_thesis: ( x <= k & k <= y & k in the carrier of (CompactSublatt L) implies x << y ) assume that A1: ( x <= k & k <= y ) and A2: k in the carrier of (CompactSublatt L) ; ::_thesis: x << y k is compact by A2, Def1; then k << k by WAYBEL_3:def_2; hence x << y by A1, WAYBEL_3:2; ::_thesis: verum end; theorem :: WAYBEL_8:2 for L being complete LATTICE for x being Element of L holds ( uparrow x is Open Filter of L iff x is compact ) proof let L be complete LATTICE; ::_thesis: for x being Element of L holds ( uparrow x is Open Filter of L iff x is compact ) let x be Element of L; ::_thesis: ( uparrow x is Open Filter of L iff x is compact ) thus ( uparrow x is Open Filter of L implies x is compact ) ::_thesis: ( x is compact implies uparrow x is Open Filter of L ) proof x <= x ; then A1: x in uparrow x by WAYBEL_0:18; assume uparrow x is Open Filter of L ; ::_thesis: x is compact then consider y being Element of L such that A2: y in uparrow x and A3: y << x by A1, WAYBEL_6:def_1; x <= y by A2, WAYBEL_0:18; then x << x by A3, WAYBEL_3:2; hence x is compact by WAYBEL_3:def_2; ::_thesis: verum end; assume A4: x is compact ; ::_thesis: uparrow x is Open Filter of L now__::_thesis:_for_u_being_Element_of_L_st_u_in_uparrow_x_holds_ ex_x2_being_Element_of_L_st_ (_x2_in_uparrow_x_&_x2_<<_u_) let u be Element of L; ::_thesis: ( u in uparrow x implies ex x2 being Element of L st ( x2 in uparrow x & x2 << u ) ) assume u in uparrow x ; ::_thesis: ex x2 being Element of L st ( x2 in uparrow x & x2 << u ) then A5: x <= u by WAYBEL_0:18; take x2 = x; ::_thesis: ( x2 in uparrow x & x2 << u ) x <= x2 ; hence x2 in uparrow x by WAYBEL_0:18; ::_thesis: x2 << u x << x by A4, WAYBEL_3:def_2; hence x2 << u by A5, WAYBEL_3:2; ::_thesis: verum end; hence uparrow x is Open Filter of L by WAYBEL_6:def_1; ::_thesis: verum end; theorem :: WAYBEL_8:3 for L being non empty with_suprema lower-bounded Poset holds ( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) ) proof let L be non empty with_suprema lower-bounded Poset; ::_thesis: ( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) ) now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(CompactSublatt_L)_&_y_in_the_carrier_of_(CompactSublatt_L)_&_ex_sup_of_{x,y},L_holds_ sup_{x,y}_in_the_carrier_of_(CompactSublatt_L) let x, y be Element of L; ::_thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_sup_of {x,y},L implies sup {x,y} in the carrier of (CompactSublatt L) ) assume that A1: x in the carrier of (CompactSublatt L) and A2: y in the carrier of (CompactSublatt L) and A3: ex_sup_of {x,y},L ; ::_thesis: sup {x,y} in the carrier of (CompactSublatt L) y is compact by A2, Def1; then A4: y << y by WAYBEL_3:def_2; x is compact by A1, Def1; then A5: x << x by WAYBEL_3:def_2; y <= x "\/" y by A3, YELLOW_0:18; then A6: y << x "\/" y by A4, WAYBEL_3:2; x <= x "\/" y by A3, YELLOW_0:18; then x << x "\/" y by A5, WAYBEL_3:2; then x "\/" y << x "\/" y by A6, WAYBEL_3:3; then x "\/" y is compact by WAYBEL_3:def_2; then sup {x,y} is compact by YELLOW_0:41; hence sup {x,y} in the carrier of (CompactSublatt L) by Def1; ::_thesis: verum end; hence CompactSublatt L is join-inheriting by YELLOW_0:def_17; ::_thesis: Bottom L in the carrier of (CompactSublatt L) Bottom L is compact by WAYBEL_3:15; hence Bottom L in the carrier of (CompactSublatt L) by Def1; ::_thesis: verum end; definition let L be non empty reflexive RelStr ; let x be Element of L; func compactbelow x -> Subset of L equals :: WAYBEL_8:def 2 { y where y is Element of L : ( x >= y & y is compact ) } ; coherence { y where y is Element of L : ( x >= y & y is compact ) } is Subset of L proof set Z = { y where y is Element of L : ( x >= y & y is compact ) } ; defpred S1[ Element of L] means ( x >= \$1 & \$1 is compact ); consider X being Subset of L such that A1: for y being Element of L holds ( y in X iff S1[y] ) from SUBSET_1:sch_3(); now__::_thesis:_for_z_being_set_holds_ (_(_z_in_X_implies_z_in__{__y_where_y_is_Element_of_L_:_(_x_>=_y_&_y_is_compact_)__}__)_&_(_z_in__{__y_where_y_is_Element_of_L_:_(_x_>=_y_&_y_is_compact_)__}__implies_z_in_X_)_) let z be set ; ::_thesis: ( ( z in X implies z in { y where y is Element of L : ( x >= y & y is compact ) } ) & ( z in { y where y is Element of L : ( x >= y & y is compact ) } implies z in X ) ) thus ( z in X implies z in { y where y is Element of L : ( x >= y & y is compact ) } ) ::_thesis: ( z in { y where y is Element of L : ( x >= y & y is compact ) } implies z in X ) proof assume A2: z in X ; ::_thesis: z in { y where y is Element of L : ( x >= y & y is compact ) } then reconsider z1 = z as Element of L ; ( x >= z1 & z1 is compact ) by A1, A2; hence z in { y where y is Element of L : ( x >= y & y is compact ) } ; ::_thesis: verum end; thus ( z in { y where y is Element of L : ( x >= y & y is compact ) } implies z in X ) ::_thesis: verum proof assume z in { y where y is Element of L : ( x >= y & y is compact ) } ; ::_thesis: z in X then ex v being Element of L st ( v = z & x >= v & v is compact ) ; hence z in X by A1; ::_thesis: verum end; end; hence { y where y is Element of L : ( x >= y & y is compact ) } is Subset of L by TARSKI:1; ::_thesis: verum end; end; :: deftheorem defines compactbelow WAYBEL_8:def_2_:_ for L being non empty reflexive RelStr for x being Element of L holds compactbelow x = { y where y is Element of L : ( x >= y & y is compact ) } ; theorem Th4: :: WAYBEL_8:4 for L being non empty reflexive RelStr for x, y being Element of L holds ( y in compactbelow x iff ( x >= y & y is compact ) ) proof let L be non empty reflexive RelStr ; ::_thesis: for x, y being Element of L holds ( y in compactbelow x iff ( x >= y & y is compact ) ) let x, y be Element of L; ::_thesis: ( y in compactbelow x iff ( x >= y & y is compact ) ) thus ( y in compactbelow x implies ( x >= y & y is compact ) ) ::_thesis: ( x >= y & y is compact implies y in compactbelow x ) proof assume y in compactbelow x ; ::_thesis: ( x >= y & y is compact ) then ex z being Element of L st ( z = y & x >= z & z is compact ) ; hence ( x >= y & y is compact ) ; ::_thesis: verum end; assume ( x >= y & y is compact ) ; ::_thesis: y in compactbelow x hence y in compactbelow x ; ::_thesis: verum end; theorem Th5: :: WAYBEL_8:5 for L being non empty reflexive RelStr for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) proof let L be non empty reflexive RelStr ; ::_thesis: for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) let x be Element of L; ::_thesis: compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) now__::_thesis:_for_y_being_set_st_y_in_(downarrow_x)_/\_the_carrier_of_(CompactSublatt_L)_holds_ y_in_compactbelow_x let y be set ; ::_thesis: ( y in (downarrow x) /\ the carrier of (CompactSublatt L) implies y in compactbelow x ) assume A1: y in (downarrow x) /\ the carrier of (CompactSublatt L) ; ::_thesis: y in compactbelow x then reconsider y9 = y as Element of L ; y in downarrow x by A1, XBOOLE_0:def_4; then A2: y9 <= x by WAYBEL_0:17; y in the carrier of (CompactSublatt L) by A1, XBOOLE_0:def_4; then y9 is compact by Def1; hence y in compactbelow x by A2; ::_thesis: verum end; then A3: (downarrow x) /\ the carrier of (CompactSublatt L) c= compactbelow x by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in_compactbelow_x_holds_ y_in_(downarrow_x)_/\_the_carrier_of_(CompactSublatt_L) let y be set ; ::_thesis: ( y in compactbelow x implies y in (downarrow x) /\ the carrier of (CompactSublatt L) ) assume y in compactbelow x ; ::_thesis: y in (downarrow x) /\ the carrier of (CompactSublatt L) then consider y9 being Element of L such that A4: y9 = y and A5: ( y9 <= x & y9 is compact ) ; ( y9 in downarrow x & y9 in the carrier of (CompactSublatt L) ) by A5, Def1, WAYBEL_0:17; hence y in (downarrow x) /\ the carrier of (CompactSublatt L) by A4, XBOOLE_0:def_4; ::_thesis: verum end; then compactbelow x c= (downarrow x) /\ the carrier of (CompactSublatt L) by TARSKI:def_3; hence compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th6: :: WAYBEL_8:6 for L being non empty reflexive transitive RelStr for x being Element of L holds compactbelow x c= waybelow x proof let L be non empty reflexive transitive RelStr ; ::_thesis: for x being Element of L holds compactbelow x c= waybelow x let x be Element of L; ::_thesis: compactbelow x c= waybelow x now__::_thesis:_for_z_being_set_st_z_in_compactbelow_x_holds_ z_in_waybelow_x let z be set ; ::_thesis: ( z in compactbelow x implies z in waybelow x ) assume z in compactbelow x ; ::_thesis: z in waybelow x then consider z9 being Element of L such that A1: z9 = z and A2: x >= z9 and A3: z9 is compact ; z9 << z9 by A3, WAYBEL_3:def_2; then z9 << x by A2, WAYBEL_3:2; hence z in waybelow x by A1, WAYBEL_3:7; ::_thesis: verum end; hence compactbelow x c= waybelow x by TARSKI:def_3; ::_thesis: verum end; registration let L be non empty reflexive antisymmetric lower-bounded RelStr ; let x be Element of L; cluster compactbelow x -> non empty ; coherence not compactbelow x is empty proof ( x >= Bottom L & Bottom L is compact ) by WAYBEL_3:15, YELLOW_0:44; then Bottom L in { y where y is Element of L : ( x >= y & y is compact ) } ; hence not compactbelow x is empty ; ::_thesis: verum end; end; begin definition let L be non empty reflexive RelStr ; attrL is satisfying_axiom_K means :Def3: :: WAYBEL_8:def 3 for x being Element of L holds x = sup (compactbelow x); end; :: deftheorem Def3 defines satisfying_axiom_K WAYBEL_8:def_3_:_ for L being non empty reflexive RelStr holds ( L is satisfying_axiom_K iff for x being Element of L holds x = sup (compactbelow x) ); definition let L be non empty reflexive RelStr ; attrL is algebraic means :Def4: :: WAYBEL_8:def 4 ( ( for x being Element of L holds ( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K ); end; :: deftheorem Def4 defines algebraic WAYBEL_8:def_4_:_ for L being non empty reflexive RelStr holds ( L is algebraic iff ( ( for x being Element of L holds ( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K ) ); theorem Th7: :: WAYBEL_8:7 for L being LATTICE holds ( L is algebraic iff ( L is continuous & ( for x, y being Element of L st x << y holds ex k being Element of L st ( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) ) proof let L be LATTICE; ::_thesis: ( L is algebraic iff ( L is continuous & ( for x, y being Element of L st x << y holds ex k being Element of L st ( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) ) thus ( L is algebraic implies ( L is continuous & ( for x, y being Element of L st x << y holds ex k being Element of L st ( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) ) ::_thesis: ( L is continuous & ( for x, y being Element of L st x << y holds ex k being Element of L st ( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) implies L is algebraic ) proof assume A1: L is algebraic ; ::_thesis: ( L is continuous & ( for x, y being Element of L st x << y holds ex k being Element of L st ( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) then A2: ( L is up-complete & L is satisfying_axiom_K ) by Def4; now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_(waybelow_x) let x be Element of L; ::_thesis: x = sup (waybelow x) A3: ( not compactbelow x is empty & compactbelow x is directed ) by A1, Def4; then A4: ex s being set st s in compactbelow x by XBOOLE_0:def_1; compactbelow x c= waybelow x by Th6; then A5: ex_sup_of waybelow x,L by A2, A4, WAYBEL_0:75; ex_sup_of compactbelow x,L by A2, A3, WAYBEL_0:75; then sup (compactbelow x) <= sup (waybelow x) by A5, Th6, YELLOW_0:34; then A6: x <= sup (waybelow x) by A2, Def3; waybelow x is_<=_than x by WAYBEL_3:9; then sup (waybelow x) <= x by A5, YELLOW_0:def_9; hence x = sup (waybelow x) by A6, ORDERS_2:2; ::_thesis: verum end; then A7: L is satisfying_axiom_of_approximation by WAYBEL_3:def_5; for x being Element of L holds ( not waybelow x is empty & waybelow x is directed ) proof let x be Element of L; ::_thesis: ( not waybelow x is empty & waybelow x is directed ) compactbelow x c= waybelow x by Th6; hence ( not waybelow x is empty & waybelow x is directed ) by A1, Def4; ::_thesis: verum end; hence L is continuous by A2, A7, WAYBEL_3:def_6; ::_thesis: for x, y being Element of L st x << y holds ex k being Element of L st ( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) let x, y be Element of L; ::_thesis: ( x << y implies ex k being Element of L st ( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) reconsider D = compactbelow y as non empty directed Subset of L by A1, Def4; assume A8: x << y ; ::_thesis: ex k being Element of L st ( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) y = sup D by A2, Def3; then consider d being Element of L such that A9: d in D and A10: x <= d by A8, WAYBEL_3:def_1; take d ; ::_thesis: ( d in the carrier of (CompactSublatt L) & x <= d & d <= y ) d is compact by A9, Th4; hence d in the carrier of (CompactSublatt L) by Def1; ::_thesis: ( x <= d & d <= y ) thus ( x <= d & d <= y ) by A9, A10, Th4; ::_thesis: verum end; assume that A11: L is continuous and A12: for x, y being Element of L st x << y holds ex k being Element of L st ( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ; ::_thesis: L is algebraic now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_(compactbelow_x) let x be Element of L; ::_thesis: x = sup (compactbelow x) A13: now__::_thesis:_for_z_being_Element_of_L_holds_ (_(_z_is_>=_than_waybelow_x_implies_z_is_>=_than_compactbelow_x_)_&_(_z_is_>=_than_compactbelow_x_implies_z_is_>=_than_waybelow_x_)_) let z be Element of L; ::_thesis: ( ( z is_>=_than waybelow x implies z is_>=_than compactbelow x ) & ( z is_>=_than compactbelow x implies z is_>=_than waybelow x ) ) thus ( z is_>=_than waybelow x implies z is_>=_than compactbelow x ) ::_thesis: ( z is_>=_than compactbelow x implies z is_>=_than waybelow x ) proof assume A14: z is_>=_than waybelow x ; ::_thesis: z is_>=_than compactbelow x now__::_thesis:_for_d_being_Element_of_L_st_d_in_compactbelow_x_holds_ d_<=_z let d be Element of L; ::_thesis: ( d in compactbelow x implies d <= z ) assume A15: d in compactbelow x ; ::_thesis: d <= z then d is compact by Th4; then A16: d << d by WAYBEL_3:def_2; d <= x by A15, Th4; then d << x by A16, WAYBEL_3:2; then d in waybelow x by WAYBEL_3:7; hence d <= z by A14, LATTICE3:def_9; ::_thesis: verum end; hence z is_>=_than compactbelow x by LATTICE3:def_9; ::_thesis: verum end; thus ( z is_>=_than compactbelow x implies z is_>=_than waybelow x ) ::_thesis: verum proof assume A17: z is_>=_than compactbelow x ; ::_thesis: z is_>=_than waybelow x now__::_thesis:_for_d_being_Element_of_L_st_d_in_waybelow_x_holds_ d_<=_z let d be Element of L; ::_thesis: ( d in waybelow x implies d <= z ) assume d in waybelow x ; ::_thesis: d <= z then d << x by WAYBEL_3:7; then consider k being Element of L such that A18: k in the carrier of (CompactSublatt L) and A19: d <= k and A20: k <= x by A12; k is compact by A18, Def1; then k in compactbelow x by A20; then k <= z by A17, LATTICE3:def_9; hence d <= z by A19, ORDERS_2:3; ::_thesis: verum end; hence z is_>=_than waybelow x by LATTICE3:def_9; ::_thesis: verum end; end; ( x = sup (waybelow x) & ex_sup_of waybelow x,L ) by A11, WAYBEL_0:75, WAYBEL_3:def_5; hence x = sup (compactbelow x) by A13, YELLOW_0:47; ::_thesis: verum end; then A21: L is satisfying_axiom_K by Def3; for x being Element of L holds ( not compactbelow x is empty & compactbelow x is directed ) proof let x be Element of L; ::_thesis: ( not compactbelow x is empty & compactbelow x is directed ) now__::_thesis:_for_Y_being_finite_Subset_of_(compactbelow_x)_ex_c_being_Element_of_L_st_ (_c_in_compactbelow_x_&_c_is_>=_than_Y_) let Y be finite Subset of (compactbelow x); ::_thesis: ex c being Element of L st ( c in compactbelow x & c is_>=_than Y ) compactbelow x c= waybelow x by Th6; then Y is finite Subset of (waybelow x) by XBOOLE_1:1; then consider b being Element of L such that A22: b in waybelow x and A23: b is_>=_than Y by A11, WAYBEL_0:1; b << x by A22, WAYBEL_3:7; then consider c being Element of L such that A24: c in the carrier of (CompactSublatt L) and A25: b <= c and A26: c <= x by A12; take c = c; ::_thesis: ( c in compactbelow x & c is_>=_than Y ) c is compact by A24, Def1; hence c in compactbelow x by A26; ::_thesis: c is_>=_than Y thus c is_>=_than Y by A23, A25, YELLOW_0:4; ::_thesis: verum end; hence ( not compactbelow x is empty & compactbelow x is directed ) by WAYBEL_0:1; ::_thesis: verum end; hence L is algebraic by A11, A21, Def4; ::_thesis: verum end; registration cluster reflexive transitive antisymmetric with_suprema with_infima algebraic -> continuous for RelStr ; coherence for b1 being LATTICE st b1 is algebraic holds b1 is continuous by Th7; end; registration cluster non empty reflexive algebraic -> non empty reflexive up-complete satisfying_axiom_K for RelStr ; coherence for b1 being non empty reflexive RelStr st b1 is algebraic holds ( b1 is up-complete & b1 is satisfying_axiom_K ) by Def4; end; registration let L be non empty with_suprema Poset; cluster CompactSublatt L -> strict full join-inheriting ; coherence CompactSublatt L is join-inheriting proof now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(CompactSublatt_L)_&_y_in_the_carrier_of_(CompactSublatt_L)_&_ex_sup_of_{x,y},L_holds_ sup_{x,y}_in_the_carrier_of_(CompactSublatt_L) let x, y be Element of L; ::_thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_sup_of {x,y},L implies sup {x,y} in the carrier of (CompactSublatt L) ) assume that A1: x in the carrier of (CompactSublatt L) and A2: y in the carrier of (CompactSublatt L) and A3: ex_sup_of {x,y},L ; ::_thesis: sup {x,y} in the carrier of (CompactSublatt L) y is compact by A2, Def1; then A4: y << y by WAYBEL_3:def_2; x is compact by A1, Def1; then A5: x << x by WAYBEL_3:def_2; y <= x "\/" y by A3, YELLOW_0:18; then A6: y << x "\/" y by A4, WAYBEL_3:2; x <= x "\/" y by A3, YELLOW_0:18; then x << x "\/" y by A5, WAYBEL_3:2; then x "\/" y << x "\/" y by A6, WAYBEL_3:3; then x "\/" y is compact by WAYBEL_3:def_2; then sup {x,y} is compact by YELLOW_0:41; hence sup {x,y} in the carrier of (CompactSublatt L) by Def1; ::_thesis: verum end; hence CompactSublatt L is join-inheriting by YELLOW_0:def_17; ::_thesis: verum end; end; definition let L be non empty reflexive RelStr ; attrL is arithmetic means :Def5: :: WAYBEL_8:def 5 ( L is algebraic & CompactSublatt L is meet-inheriting ); end; :: deftheorem Def5 defines arithmetic WAYBEL_8:def_5_:_ for L being non empty reflexive RelStr holds ( L is arithmetic iff ( L is algebraic & CompactSublatt L is meet-inheriting ) ); begin registration cluster reflexive transitive antisymmetric with_suprema with_infima arithmetic -> algebraic for RelStr ; coherence for b1 being LATTICE st b1 is arithmetic holds b1 is algebraic by Def5; end; registration cluster trivial reflexive transitive antisymmetric with_suprema with_infima -> arithmetic for RelStr ; coherence for b1 being LATTICE st b1 is trivial holds b1 is arithmetic proof let L be LATTICE; ::_thesis: ( L is trivial implies L is arithmetic ) assume A1: L is trivial ; ::_thesis: L is arithmetic reconsider L9 = L as 1 -element LATTICE by A1; A2: for x, y being Element of L9 st x << y holds ex k being Element of L9 st ( k in the carrier of (CompactSublatt L9) & x <= k & k <= y ) proof let x, y be Element of L9; ::_thesis: ( x << y implies ex k being Element of L9 st ( k in the carrier of (CompactSublatt L9) & x <= k & k <= y ) ) assume A3: x << y ; ::_thesis: ex k being Element of L9 st ( k in the carrier of (CompactSublatt L9) & x <= k & k <= y ) take k = x; ::_thesis: ( k in the carrier of (CompactSublatt L9) & x <= k & k <= y ) x = y by STRUCT_0:def_10; then k is compact by A3, WAYBEL_3:def_2; hence k in the carrier of (CompactSublatt L9) by Def1; ::_thesis: ( x <= k & k <= y ) thus ( x <= k & k <= y ) by STRUCT_0:def_10; ::_thesis: verum end; A4: L9 is algebraic by Th7, A2; for z, v being Element of L9 st z in the carrier of (CompactSublatt L9) & v in the carrier of (CompactSublatt L9) & ex_inf_of {z,v},L9 holds inf {z,v} in the carrier of (CompactSublatt L9) by STRUCT_0:def_10; then CompactSublatt L9 is meet-inheriting by YELLOW_0:def_16; hence L is arithmetic by A4, Def5; ::_thesis: verum end; end; registration cluster non empty 1 -element strict reflexive transitive antisymmetric with_suprema with_infima for RelStr ; existence ex b1 being LATTICE st ( b1 is 1 -element & b1 is strict ) proof set B = the 1 -element strict reflexive RelStr ; take the 1 -element strict reflexive RelStr ; ::_thesis: ( the 1 -element strict reflexive RelStr is 1 -element & the 1 -element strict reflexive RelStr is strict ) thus ( the 1 -element strict reflexive RelStr is 1 -element & the 1 -element strict reflexive RelStr is strict ) ; ::_thesis: verum end; end; theorem Th8: :: WAYBEL_8:8 for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds for x1, y1 being Element of L1 for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds x2 << y2 proof let L1, L2 be non empty reflexive antisymmetric RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete implies for x1, y1 being Element of L1 for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds x2 << y2 ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: L1 is up-complete ; ::_thesis: for x1, y1 being Element of L1 for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds x2 << y2 let x1, y1 be Element of L1; ::_thesis: for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds x2 << y2 let x2, y2 be Element of L2; ::_thesis: ( x1 = x2 & y1 = y2 & x1 << y1 implies x2 << y2 ) assume that A3: x1 = x2 and A4: y1 = y2 and A5: x1 << y1 ; ::_thesis: x2 << y2 now__::_thesis:_for_D2_being_non_empty_directed_Subset_of_L2_st_y2_<=_sup_D2_holds_ ex_d2_being_Element_of_L2_st_ (_d2_in_D2_&_x2_<=_d2_) let D2 be non empty directed Subset of L2; ::_thesis: ( y2 <= sup D2 implies ex d2 being Element of L2 st ( d2 in D2 & x2 <= d2 ) ) reconsider D1 = D2 as Subset of L1 by A1; reconsider D1 = D1 as non empty directed Subset of L1 by A1, WAYBEL_0:3; ex_sup_of D1,L1 by A2, WAYBEL_0:75; then A6: sup D1 = sup D2 by A1, YELLOW_0:26; assume y2 <= sup D2 ; ::_thesis: ex d2 being Element of L2 st ( d2 in D2 & x2 <= d2 ) then y1 <= sup D1 by A1, A4, A6, YELLOW_0:1; then consider d1 being Element of L1 such that A7: d1 in D1 and A8: x1 <= d1 by A5, WAYBEL_3:def_1; reconsider d2 = d1 as Element of L2 by A1; take d2 = d2; ::_thesis: ( d2 in D2 & x2 <= d2 ) thus d2 in D2 by A7; ::_thesis: x2 <= d2 thus x2 <= d2 by A1, A3, A8, YELLOW_0:1; ::_thesis: verum end; hence x2 << y2 by WAYBEL_3:def_1; ::_thesis: verum end; theorem Th9: :: WAYBEL_8:9 for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds for x being Element of L1 for y being Element of L2 st x = y & x is compact holds y is compact proof let L1, L2 be non empty reflexive antisymmetric RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete implies for x being Element of L1 for y being Element of L2 st x = y & x is compact holds y is compact ) assume A1: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete ) ; ::_thesis: for x being Element of L1 for y being Element of L2 st x = y & x is compact holds y is compact let x be Element of L1; ::_thesis: for y being Element of L2 st x = y & x is compact holds y is compact let y be Element of L2; ::_thesis: ( x = y & x is compact implies y is compact ) assume that A2: x = y and A3: x is compact ; ::_thesis: y is compact x << x by A3, WAYBEL_3:def_2; then y << y by A1, A2, Th8; hence y is compact by WAYBEL_3:def_2; ::_thesis: verum end; theorem Th10: :: WAYBEL_8:10 for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds for x being Element of L1 for y being Element of L2 st x = y holds compactbelow x = compactbelow y proof let L1, L2 be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for x being Element of L1 for y being Element of L2 st x = y holds compactbelow x = compactbelow y ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for x being Element of L1 for y being Element of L2 st x = y holds compactbelow x = compactbelow y let x be Element of L1; ::_thesis: for y being Element of L2 st x = y holds compactbelow x = compactbelow y let y be Element of L2; ::_thesis: ( x = y implies compactbelow x = compactbelow y ) assume A2: x = y ; ::_thesis: compactbelow x = compactbelow y now__::_thesis:_for_z_being_set_st_z_in_compactbelow_y_holds_ z_in_compactbelow_x let z be set ; ::_thesis: ( z in compactbelow y implies z in compactbelow x ) assume A3: z in compactbelow y ; ::_thesis: z in compactbelow x then reconsider z2 = z as Element of L2 ; reconsider z1 = z2 as Element of L1 by A1; z2 is compact by A3, Th4; then A4: z1 is compact by A1, Th9; z2 <= y by A3, Th4; then z1 <= x by A1, A2, YELLOW_0:1; hence z in compactbelow x by A4; ::_thesis: verum end; then A5: compactbelow y c= compactbelow x by TARSKI:def_3; now__::_thesis:_for_z_being_set_st_z_in_compactbelow_x_holds_ z_in_compactbelow_y let z be set ; ::_thesis: ( z in compactbelow x implies z in compactbelow y ) assume A6: z in compactbelow x ; ::_thesis: z in compactbelow y then reconsider z1 = z as Element of L1 ; reconsider z2 = z1 as Element of L2 by A1; z1 is compact by A6, Th4; then A7: z2 is compact by A1, Th9; z1 <= x by A6, Th4; then z2 <= y by A1, A2, YELLOW_0:1; hence z in compactbelow y by A7; ::_thesis: verum end; then compactbelow x c= compactbelow y by TARSKI:def_3; hence compactbelow x = compactbelow y by A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: WAYBEL_8:11 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & not L1 is empty holds not L2 is empty ; theorem Th12: :: WAYBEL_8:12 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is reflexive holds L2 is reflexive proof let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is reflexive implies L2 is reflexive ) assume A1: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & the InternalRel of L1 is_reflexive_in the carrier of L1 ) ; :: according to ORDERS_2:def_2 ::_thesis: L2 is reflexive let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of L2 or [x,x] in the InternalRel of L2 ) assume x in the carrier of L2 ; ::_thesis: [x,x] in the InternalRel of L2 hence [x,x] in the InternalRel of L2 by A1, RELAT_2:def_1; ::_thesis: verum end; theorem Th13: :: WAYBEL_8:13 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is transitive holds L2 is transitive proof let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is transitive implies L2 is transitive ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: L1 is transitive ; ::_thesis: L2 is transitive now__::_thesis:_for_x,_y,_z_being_Element_of_L2_st_x_<=_y_&_y_<=_z_holds_ x_<=_z let x, y, z be Element of L2; ::_thesis: ( x <= y & y <= z implies x <= z ) reconsider x9 = x, y9 = y, z9 = z as Element of L1 by A1; assume ( x <= y & y <= z ) ; ::_thesis: x <= z then ( x9 <= y9 & y9 <= z9 ) by A1, YELLOW_0:1; then x9 <= z9 by A2, YELLOW_0:def_2; hence x <= z by A1, YELLOW_0:1; ::_thesis: verum end; hence L2 is transitive by YELLOW_0:def_2; ::_thesis: verum end; theorem Th14: :: WAYBEL_8:14 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is antisymmetric holds L2 is antisymmetric proof let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is antisymmetric implies L2 is antisymmetric ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: L1 is antisymmetric ; ::_thesis: L2 is antisymmetric now__::_thesis:_for_x,_y_being_Element_of_L2_st_x_<=_y_&_y_<=_x_holds_ x_=_y let x, y be Element of L2; ::_thesis: ( x <= y & y <= x implies x = y ) reconsider x9 = x, y9 = y as Element of L1 by A1; assume ( x <= y & y <= x ) ; ::_thesis: x = y then ( x9 <= y9 & y9 <= x9 ) by A1, YELLOW_0:1; hence x = y by A2, YELLOW_0:def_3; ::_thesis: verum end; hence L2 is antisymmetric by YELLOW_0:def_3; ::_thesis: verum end; theorem Th15: :: WAYBEL_8:15 for L1, L2 being non empty reflexive RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds L2 is up-complete proof let L1, L2 be non empty reflexive RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete implies L2 is up-complete ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: L1 is up-complete ; ::_thesis: L2 is up-complete now__::_thesis:_for_X_being_non_empty_directed_Subset_of_L2_ex_x_being_Element_of_L2_st_ (_x_is_>=_than_X_&_(_for_y_being_Element_of_L2_st_y_is_>=_than_X_holds_ x_<=_y_)_) let X be non empty directed Subset of L2; ::_thesis: ex x being Element of L2 st ( x is_>=_than X & ( for y being Element of L2 st y is_>=_than X holds x <= y ) ) reconsider X9 = X as Subset of L1 by A1; reconsider X9 = X9 as non empty directed Subset of L1 by A1, WAYBEL_0:3; consider x9 being Element of L1 such that A3: x9 is_>=_than X9 and A4: for y9 being Element of L1 st y9 is_>=_than X9 holds x9 <= y9 by A2, WAYBEL_0:def_39; reconsider x = x9 as Element of L2 by A1; take x = x; ::_thesis: ( x is_>=_than X & ( for y being Element of L2 st y is_>=_than X holds x <= y ) ) thus x is_>=_than X by A1, A3, YELLOW_0:2; ::_thesis: for y being Element of L2 st y is_>=_than X holds x <= y let y be Element of L2; ::_thesis: ( y is_>=_than X implies x <= y ) assume A5: y is_>=_than X ; ::_thesis: x <= y reconsider y9 = y as Element of L1 by A1; x9 <= y9 by A1, A4, A5, YELLOW_0:2; hence x <= y by A1, YELLOW_0:1; ::_thesis: verum end; hence L2 is up-complete by WAYBEL_0:def_39; ::_thesis: verum end; theorem Th16: :: WAYBEL_8:16 for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is satisfying_axiom_K & ( for x being Element of L1 holds ( not compactbelow x is empty & compactbelow x is directed ) ) holds L2 is satisfying_axiom_K proof let L1, L2 be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is satisfying_axiom_K & ( for x being Element of L1 holds ( not compactbelow x is empty & compactbelow x is directed ) ) implies L2 is satisfying_axiom_K ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: L1 is satisfying_axiom_K and A3: for x being Element of L1 holds ( not compactbelow x is empty & compactbelow x is directed ) ; ::_thesis: L2 is satisfying_axiom_K now__::_thesis:_for_x_being_Element_of_L2_holds_x_=_sup_(compactbelow_x) let x be Element of L2; ::_thesis: x = sup (compactbelow x) reconsider x9 = x as Element of L1 by A1; ( not compactbelow x9 is empty & compactbelow x9 is directed ) by A3; then A4: ex_sup_of compactbelow x9,L1 by WAYBEL_0:75; ( x9 = sup (compactbelow x9) & compactbelow x = compactbelow x9 ) by A1, A2, Def3, Th10; hence x = sup (compactbelow x) by A1, A4, YELLOW_0:26; ::_thesis: verum end; hence L2 is satisfying_axiom_K by Def3; ::_thesis: verum end; theorem Th17: :: WAYBEL_8:17 for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is algebraic holds L2 is algebraic proof let L1, L2 be non empty reflexive antisymmetric RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is algebraic implies L2 is algebraic ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: L1 is algebraic ; ::_thesis: L2 is algebraic A3: L2 is up-complete by A1, A2, Th15; A4: for x being Element of L2 holds ( not compactbelow x is empty & compactbelow x is directed ) proof let x be Element of L2; ::_thesis: ( not compactbelow x is empty & compactbelow x is directed ) reconsider x9 = x as Element of L1 by A1; ( not compactbelow x9 is empty & compactbelow x9 is directed ) by A2, Def4; hence ( not compactbelow x is empty & compactbelow x is directed ) by A1, A2, A3, Th10, WAYBEL_0:3; ::_thesis: verum end; for x being Element of L1 holds ( not compactbelow x is empty & compactbelow x is directed ) by A2, Def4; then L2 is satisfying_axiom_K by A1, A2, A3, Th16; hence L2 is algebraic by A3, A4, Def4; ::_thesis: verum end; theorem Th18: :: WAYBEL_8:18 for L1, L2 being LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is arithmetic holds L2 is arithmetic proof let L1, L2 be LATTICE; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is arithmetic implies L2 is arithmetic ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: L1 is arithmetic ; ::_thesis: L2 is arithmetic A3: L2 is algebraic by A1, A2, Th17; A4: CompactSublatt L1 is meet-inheriting by A2, Def5; now__::_thesis:_for_x2,_y2_being_Element_of_L2_st_x2_in_the_carrier_of_(CompactSublatt_L2)_&_y2_in_the_carrier_of_(CompactSublatt_L2)_&_ex_inf_of_{x2,y2},L2_holds_ inf_{x2,y2}_in_the_carrier_of_(CompactSublatt_L2) let x2, y2 be Element of L2; ::_thesis: ( x2 in the carrier of (CompactSublatt L2) & y2 in the carrier of (CompactSublatt L2) & ex_inf_of {x2,y2},L2 implies inf {x2,y2} in the carrier of (CompactSublatt L2) ) reconsider x1 = x2, y1 = y2 as Element of L1 by A1; assume that A5: x2 in the carrier of (CompactSublatt L2) and A6: y2 in the carrier of (CompactSublatt L2) and A7: ex_inf_of {x2,y2},L2 ; ::_thesis: inf {x2,y2} in the carrier of (CompactSublatt L2) x2 is compact by A5, Def1; then x1 is compact by A1, A3, Th9; then A8: x1 in the carrier of (CompactSublatt L1) by Def1; y2 is compact by A6, Def1; then y1 is compact by A1, A3, Th9; then A9: y1 in the carrier of (CompactSublatt L1) by Def1; ex_inf_of {x1,y1},L1 by A1, A7, YELLOW_0:14; then inf {x1,y1} in the carrier of (CompactSublatt L1) by A4, A8, A9, YELLOW_0:def_16; then A10: inf {x1,y1} is compact by Def1; inf {x1,y1} = inf {x2,y2} by A1, A7, YELLOW_0:27; then inf {x2,y2} is compact by A1, A2, A10, Th9; hence inf {x2,y2} in the carrier of (CompactSublatt L2) by Def1; ::_thesis: verum end; then CompactSublatt L2 is meet-inheriting by YELLOW_0:def_16; hence L2 is arithmetic by A3, Def5; ::_thesis: verum end; registration let L be non empty RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> non empty ; coherence not RelStr(# the carrier of L, the InternalRel of L #) is empty ; end; registration let L be non empty reflexive RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> reflexive ; coherence RelStr(# the carrier of L, the InternalRel of L #) is reflexive by Th12; end; registration let L be transitive RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> transitive ; coherence RelStr(# the carrier of L, the InternalRel of L #) is transitive by Th13; end; registration let L be antisymmetric RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> antisymmetric ; coherence RelStr(# the carrier of L, the InternalRel of L #) is antisymmetric by Th14; end; registration let L be with_infima RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> with_infima ; coherence RelStr(# the carrier of L, the InternalRel of L #) is with_infima by YELLOW_7:14; end; registration let L be with_suprema RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> with_suprema ; coherence RelStr(# the carrier of L, the InternalRel of L #) is with_suprema by YELLOW_7:15; end; registration let L be non empty reflexive up-complete RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> up-complete ; coherence RelStr(# the carrier of L, the InternalRel of L #) is up-complete by Th15; end; registration let L be non empty reflexive antisymmetric algebraic RelStr ; cluster RelStr(# the carrier of L, the InternalRel of L #) -> algebraic ; coherence RelStr(# the carrier of L, the InternalRel of L #) is algebraic by Th17; end; registration let L be arithmetic LATTICE; cluster RelStr(# the carrier of L, the InternalRel of L #) -> arithmetic ; coherence RelStr(# the carrier of L, the InternalRel of L #) is arithmetic by Th18; end; theorem :: WAYBEL_8:19 for L being algebraic LATTICE holds ( L is arithmetic iff CompactSublatt L is LATTICE ) proof let L be algebraic LATTICE; ::_thesis: ( L is arithmetic iff CompactSublatt L is LATTICE ) thus ( L is arithmetic implies CompactSublatt L is LATTICE ) ::_thesis: ( CompactSublatt L is LATTICE implies L is arithmetic ) proof set x = the Element of L; assume A1: L is arithmetic ; ::_thesis: CompactSublatt L is LATTICE not compactbelow the Element of L is empty by Def4; then consider z being set such that A2: z in compactbelow the Element of L by XBOOLE_0:def_1; ex z9 being Element of L st ( z9 = z & the Element of L >= z9 & z9 is compact ) by A2; then CompactSublatt L is non empty full meet-inheriting join-inheriting SubRelStr of L by A1, Def1, Def5; hence CompactSublatt L is LATTICE ; ::_thesis: verum end; assume A3: CompactSublatt L is LATTICE ; ::_thesis: L is arithmetic now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(CompactSublatt_L)_&_y_in_the_carrier_of_(CompactSublatt_L)_&_ex_inf_of_{x,y},L_holds_ inf_{x,y}_in_the_carrier_of_(CompactSublatt_L) let x, y be Element of L; ::_thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (CompactSublatt L) ) assume that A4: x in the carrier of (CompactSublatt L) and A5: y in the carrier of (CompactSublatt L) and ex_inf_of {x,y},L ; ::_thesis: inf {x,y} in the carrier of (CompactSublatt L) reconsider L9 = CompactSublatt L as non empty full SubRelStr of L by A4; reconsider x9 = x, y9 = y as Element of L9 by A4, A5; set X = compactbelow (inf {x,y}); reconsider c = "/\" ({x,y},L9) as Element of L by YELLOW_0:58; A6: inf {x,y} = sup (compactbelow (inf {x,y})) by Def3; ( not compactbelow (inf {x,y}) is empty & compactbelow (inf {x,y}) is directed ) by Def4; then A7: ex_sup_of compactbelow (inf {x,y}),L by WAYBEL_0:75; A8: ex_inf_of {x9,y9},L9 by A3, YELLOW_0:21; then A9: "/\" ({x,y},L9) is_<=_than {x,y} by YELLOW_0:31; now__::_thesis:_for_z_being_set_st_z_in_compactbelow_(inf_{x,y})_holds_ z_in_(compactbelow_x)_/\_(compactbelow_y) let z be set ; ::_thesis: ( z in compactbelow (inf {x,y}) implies z in (compactbelow x) /\ (compactbelow y) ) assume z in compactbelow (inf {x,y}) ; ::_thesis: z in (compactbelow x) /\ (compactbelow y) then consider z1 being Element of L such that A10: z = z1 and A11: inf {x,y} >= z1 and A12: z1 is compact ; A13: z1 <= x "/\" y by A11, YELLOW_0:40; x "/\" y <= y by YELLOW_0:23; then z1 <= y by A13, ORDERS_2:3; then A14: z in compactbelow y by A10, A12; x "/\" y <= x by YELLOW_0:23; then z1 <= x by A13, ORDERS_2:3; then z in compactbelow x by A10, A12; hence z in (compactbelow x) /\ (compactbelow y) by A14, XBOOLE_0:def_4; ::_thesis: verum end; then A15: compactbelow (inf {x,y}) c= (compactbelow x) /\ (compactbelow y) by TARSKI:def_3; now__::_thesis:_for_b9_being_Element_of_L9_st_b9_in_compactbelow_(inf_{x,y})_holds_ b9_<=_"/\"_({x,y},L9) let b9 be Element of L9; ::_thesis: ( b9 in compactbelow (inf {x,y}) implies b9 <= "/\" ({x,y},L9) ) reconsider b = b9 as Element of L by YELLOW_0:58; assume A16: b9 in compactbelow (inf {x,y}) ; ::_thesis: b9 <= "/\" ({x,y},L9) then b9 in compactbelow y by A15, XBOOLE_0:def_4; then b <= y by Th4; then A17: b9 <= y9 by YELLOW_0:60; b9 in compactbelow x by A15, A16, XBOOLE_0:def_4; then b <= x by Th4; then b9 <= x9 by YELLOW_0:60; then b9 <= x9 "/\" y9 by A8, A17, YELLOW_0:19; hence b9 <= "/\" ({x,y},L9) by A3, YELLOW_0:40; ::_thesis: verum end; then A18: compactbelow (inf {x,y}) is_<=_than "/\" ({x,y},L9) by LATTICE3:def_9; now__::_thesis:_for_d_being_set_st_d_in_compactbelow_(inf_{x,y})_holds_ d_in_the_carrier_of_L9 let d be set ; ::_thesis: ( d in compactbelow (inf {x,y}) implies d in the carrier of L9 ) assume d in compactbelow (inf {x,y}) ; ::_thesis: d in the carrier of L9 then ex d9 being Element of L st ( d9 = d & inf {x,y} >= d9 & d9 is compact ) ; hence d in the carrier of L9 by Def1; ::_thesis: verum end; then compactbelow (inf {x,y}) c= the carrier of L9 by TARSKI:def_3; then compactbelow (inf {x,y}) is_<=_than c by A18, YELLOW_0:62; then A19: sup (compactbelow (inf {x,y})) <= c by A7, YELLOW_0:30; y9 in {x,y} by TARSKI:def_2; then "/\" ({x,y},L9) <= y9 by A9, LATTICE3:def_8; then A20: c <= y by YELLOW_0:59; x9 in {x,y} by TARSKI:def_2; then "/\" ({x,y},L9) <= x9 by A9, LATTICE3:def_8; then c <= x by YELLOW_0:59; then c <= x "/\" y by A20, YELLOW_0:23; then c <= sup (compactbelow (inf {x,y})) by A6, YELLOW_0:40; then c = sup (compactbelow (inf {x,y})) by A19, ORDERS_2:2; hence inf {x,y} in the carrier of (CompactSublatt L) by A6; ::_thesis: verum end; then CompactSublatt L is meet-inheriting by YELLOW_0:def_16; hence L is arithmetic by Def5; ::_thesis: verum end; theorem Th20: :: WAYBEL_8:20 for L being lower-bounded algebraic LATTICE holds ( L is arithmetic iff L -waybelow is multiplicative ) proof let L be lower-bounded algebraic LATTICE; ::_thesis: ( L is arithmetic iff L -waybelow is multiplicative ) thus ( L is arithmetic implies L -waybelow is multiplicative ) ::_thesis: ( L -waybelow is multiplicative implies L is arithmetic ) proof assume A1: L is arithmetic ; ::_thesis: L -waybelow is multiplicative now__::_thesis:_for_a,_x,_y_being_Element_of_L_st_[a,x]_in_L_-waybelow_&_[a,y]_in_L_-waybelow_holds_ [a,(x_"/\"_y)]_in_L_-waybelow reconsider C = CompactSublatt L as non empty full meet-inheriting SubRelStr of L by A1, Def5; let a, x, y be Element of L; ::_thesis: ( [a,x] in L -waybelow & [a,y] in L -waybelow implies [a,(x "/\" y)] in L -waybelow ) assume that A2: [a,x] in L -waybelow and A3: [a,y] in L -waybelow ; ::_thesis: [a,(x "/\" y)] in L -waybelow a << x by A2, WAYBEL_4:def_1; then consider c being Element of L such that A4: c in the carrier of (CompactSublatt L) and A5: a <= c and A6: c <= x by Th7; a << y by A3, WAYBEL_4:def_1; then consider k being Element of L such that A7: k in the carrier of (CompactSublatt L) and A8: a <= k and A9: k <= y by Th7; A10: c "/\" k <= x "/\" y by A6, A9, YELLOW_3:2; reconsider c9 = c, k9 = k as Element of C by A4, A7; c9 "/\" k9 in the carrier of (CompactSublatt L) ; then c "/\" k in the carrier of (CompactSublatt L) by YELLOW_0:69; then c "/\" k is compact by Def1; then A11: c "/\" k << c "/\" k by WAYBEL_3:def_2; a "/\" a = a by YELLOW_5:2; then a <= c "/\" k by A5, A8, YELLOW_3:2; then a << x "/\" y by A10, A11, WAYBEL_3:2; hence [a,(x "/\" y)] in L -waybelow by WAYBEL_4:def_1; ::_thesis: verum end; hence L -waybelow is multiplicative by WAYBEL_7:def_7; ::_thesis: verum end; assume A12: L -waybelow is multiplicative ; ::_thesis: L is arithmetic now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(CompactSublatt_L)_&_y_in_the_carrier_of_(CompactSublatt_L)_&_ex_inf_of_{x,y},L_holds_ inf_{x,y}_in_the_carrier_of_(CompactSublatt_L) let x, y be Element of L; ::_thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (CompactSublatt L) ) assume that A13: x in the carrier of (CompactSublatt L) and A14: y in the carrier of (CompactSublatt L) and ex_inf_of {x,y},L ; ::_thesis: inf {x,y} in the carrier of (CompactSublatt L) y is compact by A14, Def1; then y << y by WAYBEL_3:def_2; then A15: [y,y] in L -waybelow by WAYBEL_4:def_1; x is compact by A13, Def1; then x << x by WAYBEL_3:def_2; then [x,x] in L -waybelow by WAYBEL_4:def_1; then [(x "/\" y),(x "/\" y)] in L -waybelow by A12, A15, WAYBEL_7:41; then x "/\" y << x "/\" y by WAYBEL_4:def_1; then x "/\" y is compact by WAYBEL_3:def_2; then x "/\" y in the carrier of (CompactSublatt L) by Def1; hence inf {x,y} in the carrier of (CompactSublatt L) by YELLOW_0:40; ::_thesis: verum end; then CompactSublatt L is meet-inheriting by YELLOW_0:def_16; hence L is arithmetic by Def5; ::_thesis: verum end; theorem :: WAYBEL_8:21 for L being lower-bounded arithmetic LATTICE for p being Element of L st p is pseudoprime holds p is prime proof let L be lower-bounded arithmetic LATTICE; ::_thesis: for p being Element of L st p is pseudoprime holds p is prime let p be Element of L; ::_thesis: ( p is pseudoprime implies p is prime ) L -waybelow is multiplicative by Th20; hence ( p is pseudoprime implies p is prime ) by WAYBEL_7:45; ::_thesis: verum end; theorem :: WAYBEL_8:22 for L being lower-bounded distributive algebraic LATTICE st ( for p being Element of L st p is pseudoprime holds p is prime ) holds L is arithmetic proof let L be lower-bounded distributive algebraic LATTICE; ::_thesis: ( ( for p being Element of L st p is pseudoprime holds p is prime ) implies L is arithmetic ) assume for p being Element of L st p is pseudoprime holds p is prime ; ::_thesis: L is arithmetic then L -waybelow is multiplicative by WAYBEL_7:46; hence L is arithmetic by Th20; ::_thesis: verum end; registration let L be algebraic LATTICE; let c be closure Function of L,L; cluster non empty directed for Element of bool the carrier of (Image c); existence ex b1 being Subset of (Image c) st ( not b1 is empty & b1 is directed ) proof set x = the Element of (Image c); take downarrow the Element of (Image c) ; ::_thesis: ( not downarrow the Element of (Image c) is empty & downarrow the Element of (Image c) is directed ) thus ( not downarrow the Element of (Image c) is empty & downarrow the Element of (Image c) is directed ) ; ::_thesis: verum end; end; theorem Th23: :: WAYBEL_8:23 for L being algebraic LATTICE for c being closure Function of L,L st c is directed-sups-preserving holds c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) proof let L be algebraic LATTICE; ::_thesis: for c being closure Function of L,L st c is directed-sups-preserving holds c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) let c be closure Function of L,L; ::_thesis: ( c is directed-sups-preserving implies c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) ) assume A1: c is directed-sups-preserving ; ::_thesis: c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in c .: ([#] (CompactSublatt L)) or x in [#] (CompactSublatt (Image c)) ) A2: ( c is idempotent & c is monotone ) by WAYBEL_1:def_13; assume x in c .: ([#] (CompactSublatt L)) ; ::_thesis: x in [#] (CompactSublatt (Image c)) then consider y being set such that A3: y in dom c and A4: y in [#] (CompactSublatt L) and A5: x = c . y by FUNCT_1:def_6; A6: x in rng c by A3, A5, FUNCT_1:def_3; then reconsider x9 = x as Element of (Image c) by YELLOW_0:def_15; reconsider x1 = x9 as Element of L by A6; reconsider y9 = y as Element of L by A3; y9 is compact by A4, Def1; then A7: y9 << y9 by WAYBEL_3:def_2; now__::_thesis:_for_D_being_non_empty_directed_Subset_of_(Image_c)_st_x9_<=_sup_D_holds_ ex_d_being_Element_of_(Image_c)_st_ (_d_in_D_&_x9_<=_d_) id L <= c by WAYBEL_1:def_14; then (id L) . y9 <= c . y9 by YELLOW_2:9; then A8: y9 <= x1 by A5, FUNCT_1:18; let D be non empty directed Subset of (Image c); ::_thesis: ( x9 <= sup D implies ex d being Element of (Image c) st ( d in D & x9 <= d ) ) assume A9: x9 <= sup D ; ::_thesis: ex d being Element of (Image c) st ( d in D & x9 <= d ) D c= the carrier of (Image c) ; then A10: D c= rng c by YELLOW_0:def_15; then reconsider D9 = D as non empty Subset of L by XBOOLE_1:1; reconsider D9 = D9 as non empty directed Subset of L by YELLOW_2:7; A11: ex_sup_of D9,L by WAYBEL_0:75; c preserves_sup_of D9 by A1, WAYBEL_0:def_37; then A12: c . (sup D9) = sup (c .: D9) by A11, WAYBEL_0:def_31 .= sup D9 by A2, A10, YELLOW_2:20 ; c . (sup D9) = sup D by A11, WAYBEL_1:55; then x1 <= sup D9 by A9, A12, YELLOW_0:59; then y9 <= sup D9 by A8, ORDERS_2:3; then consider d9 being Element of L such that A13: d9 in D9 and A14: y9 <= d9 by A7, WAYBEL_3:def_1; reconsider d = d9 as Element of (Image c) by A13; take d = d; ::_thesis: ( d in D & x9 <= d ) thus d in D by A13; ::_thesis: x9 <= d d in the carrier of (Image c) ; then d in rng c by YELLOW_0:def_15; then d9 in { z where z is Element of L : z = c . z } by A2, YELLOW_2:19; then A15: ex z9 being Element of L st ( d9 = z9 & z9 = c . z9 ) ; c . y9 <= c . d9 by A2, A14, WAYBEL_1:def_2; hence x9 <= d by A5, A15, YELLOW_0:60; ::_thesis: verum end; then x9 << x9 by WAYBEL_3:def_1; then x9 is compact by WAYBEL_3:def_2; hence x in [#] (CompactSublatt (Image c)) by Def1; ::_thesis: verum end; theorem :: WAYBEL_8:24 for L being lower-bounded algebraic LATTICE for c being closure Function of L,L st c is directed-sups-preserving holds Image c is algebraic LATTICE proof let L be lower-bounded algebraic LATTICE; ::_thesis: for c being closure Function of L,L st c is directed-sups-preserving holds Image c is algebraic LATTICE let c be closure Function of L,L; ::_thesis: ( c is directed-sups-preserving implies Image c is algebraic LATTICE ) assume A1: c is directed-sups-preserving ; ::_thesis: Image c is algebraic LATTICE c is idempotent by WAYBEL_1:def_13; then reconsider Imc = Image c as complete LATTICE by A1, YELLOW_2:35; A2: now__::_thesis:_for_x_being_Element_of_Imc_holds_ (_not_compactbelow_x_is_empty_&_compactbelow_x_is_directed_) let x be Element of Imc; ::_thesis: ( not compactbelow x is empty & compactbelow x is directed ) now__::_thesis:_for_y,_z_being_Element_of_Imc_st_y_in_compactbelow_x_&_z_in_compactbelow_x_holds_ ex_v_being_Element_of_the_carrier_of_Imc_st_ (_v_in_compactbelow_x_&_y_<=_v_&_z_<=_v_) let y, z be Element of Imc; ::_thesis: ( y in compactbelow x & z in compactbelow x implies ex v being Element of the carrier of Imc st ( v in compactbelow x & y <= v & z <= v ) ) assume that A3: y in compactbelow x and A4: z in compactbelow x ; ::_thesis: ex v being Element of the carrier of Imc st ( v in compactbelow x & y <= v & z <= v ) y is compact by A3, Th4; then A5: y << y by WAYBEL_3:def_2; z is compact by A4, Th4; then A6: z << z by WAYBEL_3:def_2; take v = y "\/" z; ::_thesis: ( v in compactbelow x & y <= v & z <= v ) z <= v by YELLOW_0:22; then A7: z << v by A6, WAYBEL_3:2; y <= v by YELLOW_0:22; then y << v by A5, WAYBEL_3:2; then v << v by A7, WAYBEL_3:3; then A8: v is compact by WAYBEL_3:def_2; ( y <= x & z <= x ) by A3, A4, Th4; then v <= x by YELLOW_0:22; hence ( v in compactbelow x & y <= v & z <= v ) by A8, YELLOW_0:22; ::_thesis: verum end; hence ( not compactbelow x is empty & compactbelow x is directed ) by WAYBEL_0:def_1; ::_thesis: verum end; now__::_thesis:_for_x_being_Element_of_Imc_holds_x_=_sup_(compactbelow_x) let x be Element of Imc; ::_thesis: x = sup (compactbelow x) consider y being Element of L such that A9: c . y = x by YELLOW_2:10; sup (compactbelow y) in the carrier of L ; then A10: sup (compactbelow y) in dom c by FUNCT_2:def_1; ( not compactbelow y is empty & compactbelow y is directed ) by Def4; then A11: ( c preserves_sup_of compactbelow y & ex_sup_of compactbelow y,L ) by A1, WAYBEL_0:75, WAYBEL_0:def_37; then c . (sup (compactbelow y)) = sup (c .: (compactbelow y)) by WAYBEL_0:def_31; then sup (c .: (compactbelow y)) in rng c by A10, FUNCT_1:def_3; then A12: ( ex_sup_of c .: (compactbelow y),L & sup (c .: (compactbelow y)) in the carrier of (Image c) ) by YELLOW_0:17, YELLOW_0:def_15; for b being Element of Imc st b in compactbelow x holds b <= x by Th4; then x is_>=_than compactbelow x by LATTICE3:def_9; then A13: sup (compactbelow x) <= x by YELLOW_0:32; A14: c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) by A1, Th23; A15: c is monotone by A1, YELLOW_2:16; compactbelow y = (downarrow y) /\ ([#] (CompactSublatt L)) by Th5; then A16: c .: (compactbelow y) c= (c .: (downarrow y)) /\ (c .: ([#] (CompactSublatt L))) by RELAT_1:121; now__::_thesis:_for_z_being_set_st_z_in_c_.:_(compactbelow_y)_holds_ z_in_compactbelow_x let z be set ; ::_thesis: ( z in c .: (compactbelow y) implies z in compactbelow x ) assume A17: z in c .: (compactbelow y) ; ::_thesis: z in compactbelow x then consider v being set such that A18: v in dom c and A19: v in compactbelow y and A20: z = c . v by FUNCT_1:def_6; z in rng c by A18, A20, FUNCT_1:def_3; then reconsider z1 = z as Element of Imc by YELLOW_0:def_15; reconsider v = v as Element of L by A18; v <= y by A19, Th4; then c . v <= c . y by A15, WAYBEL_1:def_2; then A21: z1 <= x by A9, A20, YELLOW_0:60; z in c .: ([#] (CompactSublatt L)) by A16, A17, XBOOLE_0:def_4; then z1 is compact by A14, Def1; hence z in compactbelow x by A21; ::_thesis: verum end; then A22: c .: (compactbelow y) c= compactbelow x by TARSKI:def_3; compactbelow x is directed by A2; then A23: ex_sup_of compactbelow x,Imc by WAYBEL_0:75; c .: (compactbelow y) c= rng c by RELAT_1:111; then c .: (compactbelow y) is Subset of Imc by YELLOW_0:def_15; then A24: ( ex_sup_of c .: (compactbelow y),Imc & sup (c .: (compactbelow y)) = "\/" ((c .: (compactbelow y)),Imc) ) by A12, YELLOW_0:64; c . y = c . (sup (compactbelow y)) by Def3 .= sup (c .: (compactbelow y)) by A11, WAYBEL_0:def_31 ; then x <= sup (compactbelow x) by A9, A23, A24, A22, YELLOW_0:34; hence x = sup (compactbelow x) by A13, ORDERS_2:2; ::_thesis: verum end; then Imc is satisfying_axiom_K by Def3; hence Image c is algebraic LATTICE by A2, Def4; ::_thesis: verum end; theorem :: WAYBEL_8:25 for L being lower-bounded algebraic LATTICE for c being closure Function of L,L st c is directed-sups-preserving holds c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c)) proof let L be lower-bounded algebraic LATTICE; ::_thesis: for c being closure Function of L,L st c is directed-sups-preserving holds c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c)) let c be closure Function of L,L; ::_thesis: ( c is directed-sups-preserving implies c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c)) ) assume A1: c is directed-sups-preserving ; ::_thesis: c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c)) now__::_thesis:_for_a9_being_set_st_a9_in_[#]_(CompactSublatt_(Image_c))_holds_ a9_in_c_.:_([#]_(CompactSublatt_L)) c is idempotent by WAYBEL_1:def_13; then A2: rng c = { x where x is Element of L : x = c . x } by YELLOW_2:19; c is idempotent by WAYBEL_1:def_13; then reconsider Imc = Image c as complete LATTICE by A1, YELLOW_2:35; let a9 be set ; ::_thesis: ( a9 in [#] (CompactSublatt (Image c)) implies a9 in c .: ([#] (CompactSublatt L)) ) assume A3: a9 in [#] (CompactSublatt (Image c)) ; ::_thesis: a9 in c .: ([#] (CompactSublatt L)) A4: the carrier of (CompactSublatt Imc) c= the carrier of Imc by YELLOW_0:def_13; then reconsider a = a9 as Element of Imc by A3; a is compact by A3, Def1; then A5: a << a by WAYBEL_3:def_2; a9 in the carrier of Imc by A3, A4; then a in rng c by YELLOW_0:def_15; then consider a1 being Element of L such that A6: a = a1 and A7: a1 = c . a1 by A2; compactbelow a1 is non empty directed Subset of L by Def4; then A8: ( c preserves_sup_of compactbelow a1 & ex_sup_of compactbelow a1,L ) by A1, WAYBEL_0:75, WAYBEL_0:def_37; A9: c is monotone by A1, YELLOW_2:16; now__::_thesis:_for_z_being_set_st_z_in_c_.:_(compactbelow_a1)_holds_ z_in_(downarrow_a1)_/\_(c_.:_([#]_(CompactSublatt_L))) let z be set ; ::_thesis: ( z in c .: (compactbelow a1) implies z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) ) assume z in c .: (compactbelow a1) ; ::_thesis: z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) then consider v being set such that A10: v in dom c and A11: v in compactbelow a1 and A12: z = c . v by FUNCT_1:def_6; reconsider v9 = v as Element of L by A11; A13: v in (downarrow a1) /\ the carrier of (CompactSublatt L) by A11, Th5; then v in downarrow a1 by XBOOLE_0:def_4; then v9 <= a1 by WAYBEL_0:17; then c . v9 <= a1 by A7, A9, WAYBEL_1:def_2; then A14: z in downarrow a1 by A12, WAYBEL_0:17; v in [#] (CompactSublatt L) by A13, XBOOLE_0:def_4; then z in c .: ([#] (CompactSublatt L)) by A10, A12, FUNCT_1:def_6; hence z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) by A14, XBOOLE_0:def_4; ::_thesis: verum end; then A15: c .: (compactbelow a1) c= (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) by TARSKI:def_3; a = sup (compactbelow a1) by A6, Def3; then A16: a = sup (c .: (compactbelow a1)) by A6, A7, A8, WAYBEL_0:def_31; c .: (compactbelow a1) c= rng c by RELAT_1:111; then A17: c .: (compactbelow a1) c= the carrier of Imc by YELLOW_0:def_15; A18: (downarrow a) /\ (c .: ([#] (CompactSublatt L))) is non empty directed Subset of Imc proof (c .: ([#] (CompactSublatt L))) /\ (downarrow a) is Subset of Imc ; then reconsider D = (downarrow a) /\ (c .: ([#] (CompactSublatt L))) as Subset of Imc ; A19: Bottom Imc <= a by YELLOW_0:44; A20: now__::_thesis:_for_x,_y_being_Element_of_Imc_st_x_in_D_&_y_in_D_holds_ ex_z_being_Element_of_Imc_st_ (_z_in_D_&_x_<=_z_&_y_<=_z_) let x, y be Element of Imc; ::_thesis: ( x in D & y in D implies ex z being Element of Imc st ( z in D & x <= z & y <= z ) ) assume that A21: x in D and A22: y in D ; ::_thesis: ex z being Element of Imc st ( z in D & x <= z & y <= z ) x in c .: ([#] (CompactSublatt L)) by A21, XBOOLE_0:def_4; then consider d being set such that A23: d in dom c and A24: d in [#] (CompactSublatt L) and A25: x = c . d by FUNCT_1:def_6; y in c .: ([#] (CompactSublatt L)) by A22, XBOOLE_0:def_4; then consider e being set such that A26: e in dom c and A27: e in [#] (CompactSublatt L) and A28: y = c . e by FUNCT_1:def_6; reconsider e = e as Element of L by A26; y in downarrow a by A22, XBOOLE_0:def_4; then y <= a by WAYBEL_0:17; then A29: c . e <= a1 by A6, A28, YELLOW_0:59; reconsider d = d as Element of L by A23; A30: d <= d "\/" e by YELLOW_0:22; x in downarrow a by A21, XBOOLE_0:def_4; then x <= a by WAYBEL_0:17; then c . d <= a1 by A6, A25, YELLOW_0:59; then A31: (c . d) "\/" (c . e) <= a1 by A29, YELLOW_0:22; d "\/" e in the carrier of L ; then d "\/" e in dom c by FUNCT_2:def_1; then c . (d "\/" e) in rng c by FUNCT_1:def_3; then reconsider z = c . (d "\/" e) as Element of Imc by YELLOW_0:def_15; take z = z; ::_thesis: ( z in D & x <= z & y <= z ) A32: id L <= c by WAYBEL_1:def_14; then (id L) . e <= c . e by YELLOW_2:9; then A33: e <= c . e by FUNCT_1:18; (id L) . d <= c . d by A32, YELLOW_2:9; then d <= c . d by FUNCT_1:18; then d "\/" e <= (c . d) "\/" (c . e) by A33, YELLOW_3:3; then d "\/" e <= a1 by A31, ORDERS_2:3; then c . (d "\/" e) <= a1 by A7, A9, WAYBEL_1:def_2; then z <= a by A6, YELLOW_0:60; then A34: z in downarrow a by WAYBEL_0:17; A35: e <= d "\/" e by YELLOW_0:22; then A36: c . e <= c . (d "\/" e) by A9, WAYBEL_1:def_2; e is compact by A27, Def1; then e << e by WAYBEL_3:def_2; then A37: e << d "\/" e by A35, WAYBEL_3:2; d is compact by A24, Def1; then d << d by WAYBEL_3:def_2; then d << d "\/" e by A30, WAYBEL_3:2; then d "\/" e << d "\/" e by A37, WAYBEL_3:3; then d "\/" e is compact by WAYBEL_3:def_2; then A38: d "\/" e in [#] (CompactSublatt L) by Def1; d "\/" e in the carrier of L ; then d "\/" e in dom c by FUNCT_2:def_1; then z in c .: ([#] (CompactSublatt L)) by A38, FUNCT_1:def_6; hence z in D by A34, XBOOLE_0:def_4; ::_thesis: ( x <= z & y <= z ) c . d <= c . (d "\/" e) by A9, A30, WAYBEL_1:def_2; hence ( x <= z & y <= z ) by A25, A28, A36, YELLOW_0:60; ::_thesis: verum end; Bottom L is compact by WAYBEL_3:15; then ( dom c = the carrier of L & Bottom L in [#] (CompactSublatt L) ) by Def1, FUNCT_2:def_1; then A39: c . (Bottom L) in c .: ([#] (CompactSublatt L)) by FUNCT_1:def_6; A40: ( ex_sup_of {} ,L & {} c= the carrier of L ) by XBOOLE_1:2, YELLOW_0:42; A41: {} c= the carrier of Imc by XBOOLE_1:2; c . (Bottom L) = c . ("\/" ({},L)) by YELLOW_0:def_11 .= "\/" ({},Imc) by A40, A41, WAYBEL_1:55 .= Bottom Imc by YELLOW_0:def_11 ; then c . (Bottom L) in downarrow a by A19, WAYBEL_0:17; hence (downarrow a) /\ (c .: ([#] (CompactSublatt L))) is non empty directed Subset of Imc by A39, A20, WAYBEL_0:def_1, XBOOLE_0:def_4; ::_thesis: verum end; A42: c .: ([#] (CompactSublatt L)) c= rng c by RELAT_1:111; now__::_thesis:_for_z_being_set_st_z_in_(downarrow_a1)_/\_(c_.:_([#]_(CompactSublatt_L)))_holds_ z_in_(downarrow_a)_/\_(c_.:_([#]_(CompactSublatt_L))) let z be set ; ::_thesis: ( z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) implies z in (downarrow a) /\ (c .: ([#] (CompactSublatt L))) ) assume A43: z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) ; ::_thesis: z in (downarrow a) /\ (c .: ([#] (CompactSublatt L))) then reconsider z1 = z as Element of L ; A44: z in c .: ([#] (CompactSublatt L)) by A43, XBOOLE_0:def_4; then reconsider z2 = z1 as Element of Imc by A42, YELLOW_0:def_15; z in downarrow a1 by A43, XBOOLE_0:def_4; then z1 <= a1 by WAYBEL_0:17; then z2 <= a by A6, YELLOW_0:60; then z in downarrow a by WAYBEL_0:17; hence z in (downarrow a) /\ (c .: ([#] (CompactSublatt L))) by A44, XBOOLE_0:def_4; ::_thesis: verum end; then A45: (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) c= (downarrow a) /\ (c .: ([#] (CompactSublatt L))) by TARSKI:def_3; ex_sup_of c .: (compactbelow a1),L by A8, WAYBEL_0:def_31; then A46: a = "\/" ((c .: (compactbelow a1)),Imc) by A6, A7, A17, A16, WAYBEL_1:55; ( ex_sup_of c .: (compactbelow a1),Imc & ex_sup_of (downarrow a) /\ (c .: ([#] (CompactSublatt L))),Imc ) by YELLOW_0:17; then a <= "\/" (((downarrow a) /\ (c .: ([#] (CompactSublatt L)))),Imc) by A46, A15, A45, XBOOLE_1:1, YELLOW_0:34; then consider k being Element of Imc such that A47: k in (downarrow a) /\ (c .: ([#] (CompactSublatt L))) and A48: a <= k by A5, A18, WAYBEL_3:def_1; k in downarrow a by A47, XBOOLE_0:def_4; then A49: k <= a by WAYBEL_0:17; k in c .: ([#] (CompactSublatt L)) by A47, XBOOLE_0:def_4; hence a9 in c .: ([#] (CompactSublatt L)) by A48, A49, ORDERS_2:2; ::_thesis: verum end; then A50: [#] (CompactSublatt (Image c)) c= c .: ([#] (CompactSublatt L)) by TARSKI:def_3; c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) by A1, Th23; hence c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c)) by A50, XBOOLE_0:def_10; ::_thesis: verum end; begin theorem Th26: :: WAYBEL_8:26 for X, x being set holds ( x is Element of (BoolePoset X) iff x c= X ) proof let X, x be set ; ::_thesis: ( x is Element of (BoolePoset X) iff x c= X ) LattPOSet (BooleLatt X) = RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #) by LATTICE3:def_2; then A1: the carrier of (BoolePoset X) = the carrier of (BooleLatt X) by YELLOW_1:def_2 .= bool X by LATTICE3:def_1 ; hence ( x is Element of (BoolePoset X) implies x c= X ) ; ::_thesis: ( x c= X implies x is Element of (BoolePoset X) ) thus ( x c= X implies x is Element of (BoolePoset X) ) by A1; ::_thesis: verum end; theorem Th27: :: WAYBEL_8:27 for X being set for x, y being Element of (BoolePoset X) holds ( x << y iff for Y being Subset-Family of X st y c= union Y holds ex Z being finite Subset of Y st x c= union Z ) proof let X be set ; ::_thesis: for x, y being Element of (BoolePoset X) holds ( x << y iff for Y being Subset-Family of X st y c= union Y holds ex Z being finite Subset of Y st x c= union Z ) let x, y be Element of (BoolePoset X); ::_thesis: ( x << y iff for Y being Subset-Family of X st y c= union Y holds ex Z being finite Subset of Y st x c= union Z ) LattPOSet (BooleLatt X) = RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #) by LATTICE3:def_2; then A1: the carrier of (BoolePoset X) = the carrier of (BooleLatt X) by YELLOW_1:def_2 .= bool X by LATTICE3:def_1 ; thus ( x << y implies for Y being Subset-Family of X st y c= union Y holds ex Z being finite Subset of Y st x c= union Z ) ::_thesis: ( ( for Y being Subset-Family of X st y c= union Y holds ex Z being finite Subset of Y st x c= union Z ) implies x << y ) proof assume A2: x << y ; ::_thesis: for Y being Subset-Family of X st y c= union Y holds ex Z being finite Subset of Y st x c= union Z let Y be Subset-Family of X; ::_thesis: ( y c= union Y implies ex Z being finite Subset of Y st x c= union Z ) reconsider Y9 = Y as Subset of (BoolePoset X) by A1; assume y c= union Y ; ::_thesis: ex Z being finite Subset of Y st x c= union Z then y c= sup Y9 by YELLOW_1:21; then y <= sup Y9 by YELLOW_1:2; then consider Z being finite Subset of (BoolePoset X) such that A3: Z c= Y and A4: x <= sup Z by A2, WAYBEL_3:18; reconsider Z9 = Z as finite Subset of Y by A3; take Z9 ; ::_thesis: x c= union Z9 x c= sup Z by A4, YELLOW_1:2; hence x c= union Z9 by YELLOW_1:21; ::_thesis: verum end; thus ( ( for Y being Subset-Family of X st y c= union Y holds ex Z being finite Subset of Y st x c= union Z ) implies x << y ) ::_thesis: verum proof assume A5: for Y being Subset-Family of X st y c= union Y holds ex Z being finite Subset of Y st x c= union Z ; ::_thesis: x << y now__::_thesis:_for_Y_being_Subset_of_(BoolePoset_X)_st_y_<=_sup_Y_holds_ ex_Z_being_finite_Subset_of_(BoolePoset_X)_st_ (_Z_c=_Y_&_x_<=_sup_Z_) let Y be Subset of (BoolePoset X); ::_thesis: ( y <= sup Y implies ex Z being finite Subset of (BoolePoset X) st ( Z c= Y & x <= sup Z ) ) reconsider Y9 = Y as Subset-Family of X by A1; assume y <= sup Y ; ::_thesis: ex Z being finite Subset of (BoolePoset X) st ( Z c= Y & x <= sup Z ) then y c= sup Y by YELLOW_1:2; then y c= union Y9 by YELLOW_1:21; then consider Z9 being finite Subset of Y9 such that A6: x c= union Z9 by A5; reconsider Z = Z9 as finite Subset of (BoolePoset X) by XBOOLE_1:1; take Z = Z; ::_thesis: ( Z c= Y & x <= sup Z ) thus Z c= Y ; ::_thesis: x <= sup Z x c= sup Z by A6, YELLOW_1:21; hence x <= sup Z by YELLOW_1:2; ::_thesis: verum end; hence x << y by WAYBEL_3:19; ::_thesis: verum end; end; theorem Th28: :: WAYBEL_8:28 for X being set for x being Element of (BoolePoset X) holds ( x is finite iff x is compact ) proof let X be set ; ::_thesis: for x being Element of (BoolePoset X) holds ( x is finite iff x is compact ) let x be Element of (BoolePoset X); ::_thesis: ( x is finite iff x is compact ) percases ( x is empty or not x is empty ) ; supposeA1: x is empty ; ::_thesis: ( x is finite iff x is compact ) then x = Bottom (BoolePoset X) by YELLOW_1:18; hence ( x is finite iff x is compact ) by A1, WAYBEL_3:15; ::_thesis: verum end; supposeA2: not x is empty ; ::_thesis: ( x is finite iff x is compact ) thus ( x is finite implies x is compact ) ::_thesis: ( x is compact implies x is finite ) proof assume A3: x is finite ; ::_thesis: x is compact now__::_thesis:_for_Y_being_Subset-Family_of_X_st_x_c=_union_Y_holds_ ex_Z_being_finite_Subset_of_Y_st_x_c=_union_Z defpred S1[ set , set ] means \$1 in \$2; let Y be Subset-Family of X; ::_thesis: ( x c= union Y implies ex Z being finite Subset of Y st x c= union Z ) assume A4: x c= union Y ; ::_thesis: ex Z being finite Subset of Y st x c= union Z A5: for e being set st e in x holds ex u being set st ( u in Y & S1[e,u] ) proof let e be set ; ::_thesis: ( e in x implies ex u being set st ( u in Y & S1[e,u] ) ) assume e in x ; ::_thesis: ex u being set st ( u in Y & S1[e,u] ) then ex u being set st ( e in u & u in Y ) by A4, TARSKI:def_4; hence ex u being set st ( u in Y & S1[e,u] ) ; ::_thesis: verum end; consider f being Function such that A6: dom f = x and A7: rng f c= Y and A8: for e being set st e in x holds S1[e,f . e] from FUNCT_1:sch_5(A5); reconsider Z = rng f as Subset of Y by A7; reconsider Z = Z as finite Subset of Y by A3, A6, FINSET_1:8; take Z = Z; ::_thesis: x c= union Z now__::_thesis:_for_z_being_set_st_z_in_x_holds_ z_in_union_Z let z be set ; ::_thesis: ( z in x implies z in union Z ) assume z in x ; ::_thesis: z in union Z then ( z in f . z & f . z in Z ) by A6, A8, FUNCT_1:def_3; hence z in union Z by TARSKI:def_4; ::_thesis: verum end; hence x c= union Z by TARSKI:def_3; ::_thesis: verum end; then x << x by Th27; hence x is compact by WAYBEL_3:def_2; ::_thesis: verum end; thus ( x is compact implies x is finite ) ::_thesis: verum proof reconsider x9 = x as non empty set by A2; set Y = { {y} where y is Element of x9 : verum } ; { {y} where y is Element of x9 : verum } c= bool X proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { {y} where y is Element of x9 : verum } or t in bool X ) assume t in { {y} where y is Element of x9 : verum } ; ::_thesis: t in bool X then A9: ex y9 being Element of x9 st t = {y9} ; now__::_thesis:_for_k_being_set_st_k_in_t_holds_ k_in_X let k be set ; ::_thesis: ( k in t implies k in X ) assume A10: k in t ; ::_thesis: k in X x c= X by Th26; hence k in X by A9, A10, TARSKI:def_3; ::_thesis: verum end; then t c= X by TARSKI:def_3; hence t in bool X ; ::_thesis: verum end; then reconsider Y = { {y} where y is Element of x9 : verum } as Subset-Family of X ; now__::_thesis:_for_y_being_set_st_y_in_x_holds_ y_in_union_Y let y be set ; ::_thesis: ( y in x implies y in union Y ) assume y in x ; ::_thesis: y in union Y then A11: {y} in Y ; y in {y} by TARSKI:def_1; hence y in union Y by A11, TARSKI:def_4; ::_thesis: verum end; then A12: x c= union Y by TARSKI:def_3; assume x is compact ; ::_thesis: x is finite then x << x by WAYBEL_3:def_2; then consider Z being finite Subset of Y such that A13: x c= union Z by A12, Th27; now__::_thesis:_for_k_being_set_st_k_in_Z_holds_ k_is_finite let k be set ; ::_thesis: ( k in Z implies k is finite ) assume k in Z ; ::_thesis: k is finite then k in Y ; then ex y9 being Element of x9 st k = {y9} ; hence k is finite ; ::_thesis: verum end; then union Z is finite by FINSET_1:7; hence x is finite by A13; ::_thesis: verum end; end; end; end; theorem Th29: :: WAYBEL_8:29 for X being set for x being Element of (BoolePoset X) holds compactbelow x = { y where y is finite Subset of x : verum } proof let X be set ; ::_thesis: for x being Element of (BoolePoset X) holds compactbelow x = { y where y is finite Subset of x : verum } let x be Element of (BoolePoset X); ::_thesis: compactbelow x = { y where y is finite Subset of x : verum } now__::_thesis:_for_z_being_set_st_z_in__{__y_where_y_is_finite_Subset_of_x_:_verum__}__holds_ z_in_compactbelow_x let z be set ; ::_thesis: ( z in { y where y is finite Subset of x : verum } implies z in compactbelow x ) assume z in { y where y is finite Subset of x : verum } ; ::_thesis: z in compactbelow x then consider z9 being finite Subset of x such that A1: z9 = z ; x c= X by Th26; then z9 c= X by XBOOLE_1:1; then reconsider z1 = z9 as Element of (BoolePoset X) by Th26; ( z1 is compact & z1 <= x ) by Th28, YELLOW_1:2; hence z in compactbelow x by A1; ::_thesis: verum end; then A2: { y where y is finite Subset of x : verum } c= compactbelow x by TARSKI:def_3; now__::_thesis:_for_z_being_set_st_z_in_compactbelow_x_holds_ z_in__{__y_where_y_is_finite_Subset_of_x_:_verum__}_ let z be set ; ::_thesis: ( z in compactbelow x implies z in { y where y is finite Subset of x : verum } ) assume z in compactbelow x ; ::_thesis: z in { y where y is finite Subset of x : verum } then consider z9 being Element of (BoolePoset X) such that A3: z9 = z and A4: ( x >= z9 & z9 is compact ) ; ( z is finite & z9 c= x ) by A3, A4, Th28, YELLOW_1:2; hence z in { y where y is finite Subset of x : verum } by A3; ::_thesis: verum end; then compactbelow x c= { y where y is finite Subset of x : verum } by TARSKI:def_3; hence compactbelow x = { y where y is finite Subset of x : verum } by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: WAYBEL_8:30 for X being set for F being Subset of X holds ( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite ) proof let X be set ; ::_thesis: for F being Subset of X holds ( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite ) let F be Subset of X; ::_thesis: ( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite ) reconsider F9 = F as Element of (BoolePoset X) by Th26; A1: F c= F ; thus ( F in the carrier of (CompactSublatt (BoolePoset X)) implies F is finite ) ::_thesis: ( F is finite implies F in the carrier of (CompactSublatt (BoolePoset X)) ) proof assume A2: F in the carrier of (CompactSublatt (BoolePoset X)) ; ::_thesis: F is finite the carrier of (CompactSublatt (BoolePoset X)) c= the carrier of (BoolePoset X) by YELLOW_0:def_13; then reconsider F9 = F as Element of (BoolePoset X) by A2; ( F9 <= F9 & F9 is compact ) by A2, Def1; then F9 in compactbelow F9 ; then F9 in { y where y is finite Subset of F9 : verum } by Th29; then ex F1 being finite Subset of F9 st F1 = F9 ; hence F is finite ; ::_thesis: verum end; assume F is finite ; ::_thesis: F in the carrier of (CompactSublatt (BoolePoset X)) then F in { y where y is finite Subset of F9 : verum } by A1; then F9 in compactbelow F9 by Th29; then F9 is compact by Th4; hence F in the carrier of (CompactSublatt (BoolePoset X)) by Def1; ::_thesis: verum end; registration let X be set ; let x be Element of (BoolePoset X); cluster compactbelow x -> directed lower ; coherence ( compactbelow x is lower & compactbelow x is directed ) proof now__::_thesis:_for_a,_b_being_set_st_a_c=_b_&_b_in_compactbelow_x_holds_ a_in_compactbelow_x let a, b be set ; ::_thesis: ( a c= b & b in compactbelow x implies a in compactbelow x ) assume that A1: a c= b and A2: b in compactbelow x ; ::_thesis: a in compactbelow x b in { y where y is finite Subset of x : verum } by A2, Th29; then ex b1 being finite Subset of x st b = b1 ; then a is finite Subset of x by A1, XBOOLE_1:1; then a in { y where y is finite Subset of x : verum } ; hence a in compactbelow x by Th29; ::_thesis: verum end; hence A3: compactbelow x is lower by WAYBEL_7:6; ::_thesis: compactbelow x is directed now__::_thesis:_for_a,_b_being_set_st_a_in_compactbelow_x_&_b_in_compactbelow_x_holds_ a_\/_b_in_compactbelow_x let a, b be set ; ::_thesis: ( a in compactbelow x & b in compactbelow x implies a \/ b in compactbelow x ) assume that A4: a in compactbelow x and A5: b in compactbelow x ; ::_thesis: a \/ b in compactbelow x b in { y where y is finite Subset of x : verum } by A5, Th29; then A6: ex b1 being finite Subset of x st b = b1 ; a in { y where y is finite Subset of x : verum } by A4, Th29; then ex a1 being finite Subset of x st a = a1 ; then a \/ b is finite Subset of x by A6, XBOOLE_1:8; then a \/ b in { y where y is finite Subset of x : verum } ; hence a \/ b in compactbelow x by Th29; ::_thesis: verum end; hence compactbelow x is directed by A3, WAYBEL_7:8; ::_thesis: verum end; end; theorem Th31: :: WAYBEL_8:31 for X being set holds BoolePoset X is algebraic proof let X be set ; ::_thesis: BoolePoset X is algebraic now__::_thesis:_for_x_being_Element_of_(BoolePoset_X)_holds_x_=_sup_(compactbelow_x) let x be Element of (BoolePoset X); ::_thesis: x = sup (compactbelow x) A1: now__::_thesis:_for_a_being_Element_of_(BoolePoset_X)_st_a_is_>=_than_compactbelow_x_holds_ x_<=_a let a be Element of (BoolePoset X); ::_thesis: ( a is_>=_than compactbelow x implies x <= a ) assume A2: a is_>=_than compactbelow x ; ::_thesis: x <= a now__::_thesis:_for_t_being_set_st_t_in_x_holds_ t_in_a let t be set ; ::_thesis: ( t in x implies t in a ) assume A3: t in x ; ::_thesis: t in a A4: x c= X by Th26; now__::_thesis:_for_k_being_set_st_k_in_{t}_holds_ k_in_X let k be set ; ::_thesis: ( k in {t} implies k in X ) assume k in {t} ; ::_thesis: k in X then k = t by TARSKI:def_1; hence k in X by A3, A4; ::_thesis: verum end; then {t} c= X by TARSKI:def_3; then reconsider t1 = {t} as Element of (BoolePoset X) by Th26; for k being set st k in {t} holds k in x by A3, TARSKI:def_1; then {t} is finite Subset of x by TARSKI:def_3; then {t} in { y where y is finite Subset of x : verum } ; then {t} in compactbelow x by Th29; then t1 <= a by A2, LATTICE3:def_9; then ( t in {t} & {t} c= a ) by TARSKI:def_1, YELLOW_1:2; hence t in a ; ::_thesis: verum end; then x c= a by TARSKI:def_3; hence x <= a by YELLOW_1:2; ::_thesis: verum end; for b being Element of (BoolePoset X) st b in compactbelow x holds b <= x by Th4; then x is_>=_than compactbelow x by LATTICE3:def_9; hence x = sup (compactbelow x) by A1, YELLOW_0:32; ::_thesis: verum end; then ( ( for x being Element of (BoolePoset X) holds ( not compactbelow x is empty & compactbelow x is directed ) ) & BoolePoset X is satisfying_axiom_K ) by Def3; hence BoolePoset X is algebraic by Def4; ::_thesis: verum end; registration let X be set ; cluster BoolePoset X -> algebraic ; coherence BoolePoset X is algebraic by Th31; end;