:: WAYBEL13 semantic presentation begin theorem Th1: :: WAYBEL13:1 for L being non empty reflexive transitive RelStr for x, y being Element of L st x <= y holds compactbelow x c= compactbelow y proof let L be non empty reflexive transitive RelStr ; ::_thesis: for x, y being Element of L st x <= y holds compactbelow x c= compactbelow y let x, y be Element of L; ::_thesis: ( x <= y implies compactbelow x c= compactbelow y ) assume A1: x <= y ; ::_thesis: compactbelow x c= compactbelow y 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 z in compactbelow x ; ::_thesis: z in compactbelow y then z in { v where v is Element of L : ( x >= v & v is compact ) } by WAYBEL_8:def_2; then consider z9 being Element of L such that A2: z9 = z and A3: x >= z9 and A4: z9 is compact ; z9 <= y by A1, A3, ORDERS_2:3; hence z in compactbelow y by A2, A4, WAYBEL_8:4; ::_thesis: verum end; hence compactbelow x c= compactbelow y by TARSKI:def_3; ::_thesis: verum end; theorem Th2: :: WAYBEL13:2 for L being non empty reflexive RelStr for x being Element of L holds compactbelow x is Subset of (CompactSublatt L) proof let L be non empty reflexive RelStr ; ::_thesis: for x being Element of L holds compactbelow x is Subset of (CompactSublatt L) let x be Element of L; ::_thesis: compactbelow x is Subset of (CompactSublatt L) now__::_thesis:_for_v_being_set_st_v_in_compactbelow_x_holds_ v_in_the_carrier_of_(CompactSublatt_L) let v be set ; ::_thesis: ( v in compactbelow x implies v in the carrier of (CompactSublatt L) ) assume v in compactbelow x ; ::_thesis: v in the carrier of (CompactSublatt L) then v in { z where z is Element of L : ( x >= z & z is compact ) } by WAYBEL_8:def_2; then ex v1 being Element of L st ( v1 = v & x >= v1 & v1 is compact ) ; hence v in the carrier of (CompactSublatt L) by WAYBEL_8:def_1; ::_thesis: verum end; hence compactbelow x is Subset of (CompactSublatt L) by TARSKI:def_3; ::_thesis: verum end; theorem Th3: :: WAYBEL13:3 for L being RelStr for S being SubRelStr of L for X being Subset of S holds X is Subset of L proof let L be RelStr ; ::_thesis: for S being SubRelStr of L for X being Subset of S holds X is Subset of L let S be SubRelStr of L; ::_thesis: for X being Subset of S holds X is Subset of L let X be Subset of S; ::_thesis: X is Subset of L the carrier of S c= the carrier of L by YELLOW_0:def_13; hence X is Subset of L by XBOOLE_1:1; ::_thesis: verum end; theorem Th4: :: WAYBEL13:4 for L being non empty reflexive transitive with_suprema RelStr holds the carrier of L is Ideal of L proof let L be non empty reflexive transitive with_suprema RelStr ; ::_thesis: the carrier of L is Ideal of L [#] L is Ideal of L ; hence the carrier of L is Ideal of L ; ::_thesis: verum end; theorem Th5: :: WAYBEL13:5 for L1 being non empty reflexive antisymmetric lower-bounded RelStr for 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 the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2) proof let L1 be non empty reflexive antisymmetric lower-bounded RelStr ; ::_thesis: for 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 the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2) let 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 the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2) ) 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: the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2) now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(CompactSublatt_L2)_holds_ x_in_the_carrier_of_(CompactSublatt_L1) reconsider L29 = L2 as non empty reflexive antisymmetric lower-bounded RelStr by A1, YELLOW_0:13; let x be set ; ::_thesis: ( x in the carrier of (CompactSublatt L2) implies x in the carrier of (CompactSublatt L1) ) assume A3: x in the carrier of (CompactSublatt L2) ; ::_thesis: x in the carrier of (CompactSublatt L1) then x is Element of (CompactSublatt L29) ; then reconsider x2 = x as Element of L2 by YELLOW_0:58; reconsider x1 = x2 as Element of L1 by A1; A4: x2 is compact by A3, WAYBEL_8:def_1; L2 is up-complete by A1, A2, WAYBEL_8:15; then x1 is compact by A1, A4, WAYBEL_8:9; hence x in the carrier of (CompactSublatt L1) by WAYBEL_8:def_1; ::_thesis: verum end; then A5: the carrier of (CompactSublatt L2) c= the carrier of (CompactSublatt L1) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(CompactSublatt_L1)_holds_ x_in_the_carrier_of_(CompactSublatt_L2) let x be set ; ::_thesis: ( x in the carrier of (CompactSublatt L1) implies x in the carrier of (CompactSublatt L2) ) assume A6: x in the carrier of (CompactSublatt L1) ; ::_thesis: x in the carrier of (CompactSublatt L2) then reconsider x1 = x as Element of L1 by YELLOW_0:58; reconsider x2 = x1 as Element of L2 by A1; x1 is compact by A6, WAYBEL_8:def_1; then x2 is compact by A1, A2, WAYBEL_8:9; hence x in the carrier of (CompactSublatt L2) by WAYBEL_8:def_1; ::_thesis: verum end; then the carrier of (CompactSublatt L1) c= the carrier of (CompactSublatt L2) by TARSKI:def_3; hence the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2) by A5, XBOOLE_0:def_10; ::_thesis: verum end; begin theorem Th6: :: WAYBEL13:6 for L being lower-bounded algebraic LATTICE for S being CLSubFrame of L holds S is algebraic proof let L be lower-bounded algebraic LATTICE; ::_thesis: for S being CLSubFrame of L holds S is algebraic let S be CLSubFrame of L; ::_thesis: S is algebraic RelStr(# the carrier of S, the InternalRel of S #) = Image (closure_op S) by WAYBEL10:18; then RelStr(# the carrier of S, the InternalRel of S #) is algebraic by WAYBEL_8:24; hence S is algebraic by WAYBEL_8:17; ::_thesis: verum end; theorem Th7: :: WAYBEL13:7 for X, E being set for L being CLSubFrame of BoolePoset X holds ( E in the carrier of (CompactSublatt L) iff ex F being Element of (BoolePoset X) st ( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) ) proof let X, E be set ; ::_thesis: for L being CLSubFrame of BoolePoset X holds ( E in the carrier of (CompactSublatt L) iff ex F being Element of (BoolePoset X) st ( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) ) let L be CLSubFrame of BoolePoset X; ::_thesis: ( E in the carrier of (CompactSublatt L) iff ex F being Element of (BoolePoset X) st ( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) ) A1: the carrier of L c= the carrier of (BoolePoset X) by YELLOW_0:def_13; A2: L is complete LATTICE by YELLOW_2:30; thus ( E in the carrier of (CompactSublatt L) implies ex F being Element of (BoolePoset X) st ( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) ) ::_thesis: ( ex F being Element of (BoolePoset X) st ( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) implies E in the carrier of (CompactSublatt L) ) proof A3: (closure_op L) .: ([#] (CompactSublatt (BoolePoset X))) = [#] (CompactSublatt (Image (closure_op L))) by WAYBEL_8:25 .= [#] (CompactSublatt RelStr(# the carrier of L, the InternalRel of L #)) by WAYBEL10:18 .= the carrier of (CompactSublatt RelStr(# the carrier of L, the InternalRel of L #)) ; assume E in the carrier of (CompactSublatt L) ; ::_thesis: ex F being Element of (BoolePoset X) st ( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) then E in (closure_op L) .: ([#] (CompactSublatt (BoolePoset X))) by A2, A3, Th5; then consider x being set such that A4: x in dom (closure_op L) and A5: x in [#] (CompactSublatt (BoolePoset X)) and A6: E = (closure_op L) . x by FUNCT_1:def_6; reconsider F = x as Element of (BoolePoset X) by A4; id (BoolePoset X) <= closure_op L by WAYBEL_1:def_14; then (id (BoolePoset X)) . F <= (closure_op L) . F by YELLOW_2:9; then F <= (closure_op L) . F by FUNCT_1:18; then A7: F c= (closure_op L) . F by YELLOW_1:2; (closure_op L) . x in rng (closure_op L) by A4, FUNCT_1:def_3; then (closure_op L) . x in the carrier of (Image (closure_op L)) by YELLOW_0:def_15; then (closure_op L) . x in the carrier of RelStr(# the carrier of L, the InternalRel of L #) by WAYBEL10:18; then A8: (closure_op L) . x in { Y where Y is Element of L : F c= Y } by A7; take F ; ::_thesis: ( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) F is compact by A5, WAYBEL_8:def_1; hence F is finite by WAYBEL_8:28; ::_thesis: ( E = meet { Y where Y is Element of L : F c= Y } & F c= E ) A9: (uparrow F) /\ the carrier of L c= { Y where Y is Element of L : F c= Y } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (uparrow F) /\ the carrier of L or z in { Y where Y is Element of L : F c= Y } ) assume A10: z in (uparrow F) /\ the carrier of L ; ::_thesis: z in { Y where Y is Element of L : F c= Y } then reconsider z9 = z as Element of (BoolePoset X) ; z in uparrow F by A10, XBOOLE_0:def_4; then F <= z9 by WAYBEL_0:18; then A11: F c= z by YELLOW_1:2; z in the carrier of L by A10, XBOOLE_0:def_4; hence z in { Y where Y is Element of L : F c= Y } by A11; ::_thesis: verum end; { Y where Y is Element of L : F c= Y } c= (uparrow F) /\ the carrier of L proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { Y where Y is Element of L : F c= Y } or z in (uparrow F) /\ the carrier of L ) assume z in { Y where Y is Element of L : F c= Y } ; ::_thesis: z in (uparrow F) /\ the carrier of L then consider z9 being Element of L such that A12: z = z9 and A13: F c= z9 ; reconsider z1 = z9 as Element of (BoolePoset X) by A1, TARSKI:def_3; F <= z1 by A13, YELLOW_1:2; then z in uparrow F by A12, WAYBEL_0:18; hence z in (uparrow F) /\ the carrier of L by A12, XBOOLE_0:def_4; ::_thesis: verum end; then A14: (uparrow F) /\ the carrier of L = { Y where Y is Element of L : F c= Y } by A9, XBOOLE_0:def_10; thus A15: E = "/\" (((uparrow F) /\ the carrier of L),(BoolePoset X)) by A6, WAYBEL10:def_5 .= meet { Y where Y is Element of L : F c= Y } by A8, A14, YELLOW_1:20 ; ::_thesis: F c= E now__::_thesis:_for_v_being_set_st_v_in_F_holds_ v_in_E let v be set ; ::_thesis: ( v in F implies v in E ) assume A16: v in F ; ::_thesis: v in E now__::_thesis:_for_V_being_set_st_V_in__{__Y_where_Y_is_Element_of_L_:_F_c=_Y__}__holds_ v_in_V let V be set ; ::_thesis: ( V in { Y where Y is Element of L : F c= Y } implies v in V ) assume V in { Y where Y is Element of L : F c= Y } ; ::_thesis: v in V then ex V9 being Element of L st ( V = V9 & F c= V9 ) ; hence v in V by A16; ::_thesis: verum end; hence v in E by A8, A15, SETFAM_1:def_1; ::_thesis: verum end; hence F c= E by TARSKI:def_3; ::_thesis: verum end; thus ( ex F being Element of (BoolePoset X) st ( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) implies E in the carrier of (CompactSublatt L) ) ::_thesis: verum proof given F being Element of (BoolePoset X) such that A17: F is finite and A18: E = meet { Y where Y is Element of L : F c= Y } and F c= E ; ::_thesis: E in the carrier of (CompactSublatt L) F is compact by A17, WAYBEL_8:28; then A19: F in [#] (CompactSublatt (BoolePoset X)) by WAYBEL_8:def_1; A20: (uparrow F) /\ the carrier of L c= { Y where Y is Element of L : F c= Y } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (uparrow F) /\ the carrier of L or z in { Y where Y is Element of L : F c= Y } ) assume A21: z in (uparrow F) /\ the carrier of L ; ::_thesis: z in { Y where Y is Element of L : F c= Y } then reconsider z9 = z as Element of (BoolePoset X) ; z in uparrow F by A21, XBOOLE_0:def_4; then F <= z9 by WAYBEL_0:18; then A22: F c= z by YELLOW_1:2; z in the carrier of L by A21, XBOOLE_0:def_4; hence z in { Y where Y is Element of L : F c= Y } by A22; ::_thesis: verum end; { Y where Y is Element of L : F c= Y } c= (uparrow F) /\ the carrier of L proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { Y where Y is Element of L : F c= Y } or z in (uparrow F) /\ the carrier of L ) assume z in { Y where Y is Element of L : F c= Y } ; ::_thesis: z in (uparrow F) /\ the carrier of L then consider z9 being Element of L such that A23: z = z9 and A24: F c= z9 ; reconsider z1 = z9 as Element of (BoolePoset X) by A1, TARSKI:def_3; F <= z1 by A24, YELLOW_1:2; then z in uparrow F by A23, WAYBEL_0:18; hence z in (uparrow F) /\ the carrier of L by A23, XBOOLE_0:def_4; ::_thesis: verum end; then A25: (uparrow F) /\ the carrier of L = { Y where Y is Element of L : F c= Y } by A20, XBOOLE_0:def_10; id (BoolePoset X) <= closure_op L by WAYBEL_1:def_14; then (id (BoolePoset X)) . F <= (closure_op L) . F by YELLOW_2:9; then F <= (closure_op L) . F by FUNCT_1:18; then A26: F c= (closure_op L) . F by YELLOW_1:2; F in the carrier of (BoolePoset X) ; then A27: F in dom (closure_op L) by FUNCT_2:def_1; then (closure_op L) . F in rng (closure_op L) by FUNCT_1:def_3; then (closure_op L) . F in the carrier of (Image (closure_op L)) by YELLOW_0:def_15; then (closure_op L) . F in the carrier of RelStr(# the carrier of L, the InternalRel of L #) by WAYBEL10:18; then (closure_op L) . F in { Y where Y is Element of L : F c= Y } by A26; then E = "/\" (((uparrow F) /\ the carrier of L),(BoolePoset X)) by A18, A25, YELLOW_1:20 .= (closure_op L) . F by WAYBEL10:def_5 ; then A28: E in (closure_op L) .: ([#] (CompactSublatt (BoolePoset X))) by A27, A19, FUNCT_1:def_6; (closure_op L) .: ([#] (CompactSublatt (BoolePoset X))) = [#] (CompactSublatt (Image (closure_op L))) by WAYBEL_8:25 .= [#] (CompactSublatt RelStr(# the carrier of L, the InternalRel of L #)) by WAYBEL10:18 .= the carrier of (CompactSublatt RelStr(# the carrier of L, the InternalRel of L #)) ; hence E in the carrier of (CompactSublatt L) by A2, A28, Th5; ::_thesis: verum end; end; theorem Th8: :: WAYBEL13:8 for L being lower-bounded sup-Semilattice holds InclPoset (Ids L) is CLSubFrame of BoolePoset the carrier of L proof let L be lower-bounded sup-Semilattice; ::_thesis: InclPoset (Ids L) is CLSubFrame of BoolePoset the carrier of L now__::_thesis:_for_x_being_set_st_x_in_Ids_L_holds_ x_in_bool_the_carrier_of_L let x be set ; ::_thesis: ( x in Ids L implies x in bool the carrier of L ) assume x in Ids L ; ::_thesis: x in bool the carrier of L then x in { X where X is Ideal of L : verum } by WAYBEL_0:def_23; then ex x9 being Ideal of L st x9 = x ; hence x in bool the carrier of L ; ::_thesis: verum end; then Ids L is Subset-Family of L by TARSKI:def_3; then reconsider InIdL = InclPoset (Ids L) as non empty full SubRelStr of BoolePoset the carrier of L by YELLOW_1:5; A1: for X being directed Subset of InIdL st X <> {} & ex_sup_of X, BoolePoset the carrier of L holds "\/" (X,(BoolePoset the carrier of L)) in the carrier of InIdL proof let X be directed Subset of InIdL; ::_thesis: ( X <> {} & ex_sup_of X, BoolePoset the carrier of L implies "\/" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ) assume that A2: X <> {} and ex_sup_of X, BoolePoset the carrier of L ; ::_thesis: "\/" (X,(BoolePoset the carrier of L)) in the carrier of InIdL consider Y being set such that A3: Y in X by A2, XBOOLE_0:def_1; X is Subset of (BoolePoset the carrier of L) by Th3; then A4: "\/" (X,(BoolePoset the carrier of L)) = union X by YELLOW_1:21; then reconsider uX = union X as Subset of L by WAYBEL_8:26; Y is Ideal of L by A3, YELLOW_2:41; then Bottom L in Y by WAYBEL_4:21; then reconsider uX = uX as non empty Subset of L by A3, TARSKI:def_4; now__::_thesis:_for_z_being_set_st_z_in_X_holds_ z_in_bool_the_carrier_of_L let z be set ; ::_thesis: ( z in X implies z in bool the carrier of L ) assume z in X ; ::_thesis: z in bool the carrier of L then z is Ideal of L by YELLOW_2:41; hence z in bool the carrier of L ; ::_thesis: verum end; then A5: X c= bool the carrier of L by TARSKI:def_3; A6: now__::_thesis:_for_Y,_Z_being_Subset_of_L_st_Y_in_X_&_Z_in_X_holds_ ex_V_being_Subset_of_L_st_ (_V_in_X_&_Y_\/_Z_c=_V_) let Y, Z be Subset of L; ::_thesis: ( Y in X & Z in X implies ex V being Subset of L st ( V in X & Y \/ Z c= V ) ) assume A7: ( Y in X & Z in X ) ; ::_thesis: ex V being Subset of L st ( V in X & Y \/ Z c= V ) then reconsider Y9 = Y, Z9 = Z as Element of InIdL ; consider V9 being Element of InIdL such that A8: V9 in X and A9: ( Y9 <= V9 & Z9 <= V9 ) by A7, WAYBEL_0:def_1; reconsider V = V9 as Subset of L by YELLOW_2:41; take V = V; ::_thesis: ( V in X & Y \/ Z c= V ) thus V in X by A8; ::_thesis: Y \/ Z c= V Y9 "\/" Z9 <= V9 by A9, YELLOW_0:22; then A10: Y9 "\/" Z9 c= V9 by YELLOW_1:3; Y \/ Z c= Y9 "\/" Z9 by YELLOW_1:6; hence Y \/ Z c= V by A10, XBOOLE_1:1; ::_thesis: verum end; ( ( for Y being Subset of L st Y in X holds Y is lower ) & ( for Y being Subset of L st Y in X holds Y is directed ) ) by YELLOW_2:41; then uX is Ideal of L by A5, A6, WAYBEL_0:26, WAYBEL_0:46; then "\/" (X,(BoolePoset the carrier of L)) is Element of InIdL by A4, YELLOW_2:41; hence "\/" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ; ::_thesis: verum end; for X being Subset of InIdL st ex_inf_of X, BoolePoset the carrier of L holds "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL proof let X be Subset of InIdL; ::_thesis: ( ex_inf_of X, BoolePoset the carrier of L implies "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ) assume ex_inf_of X, BoolePoset the carrier of L ; ::_thesis: "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL now__::_thesis:_"/\"_(X,(BoolePoset_the_carrier_of_L))_in_the_carrier_of_InIdL percases ( not X is empty or X is empty ) ; supposeA11: not X is empty ; ::_thesis: "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL X is Subset of (BoolePoset the carrier of L) by Th3; then A12: "/\" (X,(BoolePoset the carrier of L)) = meet X by A11, YELLOW_1:20; InclPoset (Ids L) = RelStr(# (Ids L),(RelIncl (Ids L)) #) by YELLOW_1:def_1; then "/\" (X,(BoolePoset the carrier of L)) is Ideal of L by A11, A12, YELLOW_2:45; then "/\" (X,(BoolePoset the carrier of L)) is Element of InIdL by YELLOW_2:41; hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ; ::_thesis: verum end; supposeA13: X is empty ; ::_thesis: "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL "/\" ({},(BoolePoset the carrier of L)) = Top (BoolePoset the carrier of L) by YELLOW_0:def_12 .= the carrier of L by YELLOW_1:19 ; then "/\" ({},(BoolePoset the carrier of L)) is Ideal of L by Th4; then "/\" (X,(BoolePoset the carrier of L)) is Element of InIdL by A13, YELLOW_2:41; hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ; ::_thesis: verum end; end; end; hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ; ::_thesis: verum end; hence InclPoset (Ids L) is CLSubFrame of BoolePoset the carrier of L by A1, WAYBEL_0:def_4, YELLOW_0:def_18; ::_thesis: verum end; registration let L be non empty reflexive transitive RelStr ; cluster non empty directed lower principal for Element of K32( the carrier of L); existence ex b1 being Ideal of L st b1 is principal proof set x = the Element of L; take downarrow the Element of L ; ::_thesis: downarrow the Element of L is principal thus downarrow the Element of L is principal by WAYBEL_0:48; ::_thesis: verum end; end; theorem Th9: :: WAYBEL13:9 for L being lower-bounded sup-Semilattice for X being non empty directed Subset of (InclPoset (Ids L)) holds sup X = union X proof let L be lower-bounded sup-Semilattice; ::_thesis: for X being non empty directed Subset of (InclPoset (Ids L)) holds sup X = union X let X be non empty directed Subset of (InclPoset (Ids L)); ::_thesis: sup X = union X consider z being set such that A1: z in X by XBOOLE_0:def_1; X c= the carrier of (InclPoset (Ids L)) ; then A2: X c= Ids L by YELLOW_1:1; now__::_thesis:_for_x_being_set_st_x_in_X_holds_ x_in_bool_the_carrier_of_L let x be set ; ::_thesis: ( x in X implies x in bool the carrier of L ) assume x in X ; ::_thesis: x in bool the carrier of L then x in Ids L by A2; then x in { Y where Y is Ideal of L : verum } by WAYBEL_0:def_23; then ex x1 being Ideal of L st x = x1 ; hence x in bool the carrier of L ; ::_thesis: verum end; then A3: X c= bool the carrier of L by TARSKI:def_3; now__::_thesis:_for_Z_being_Subset_of_L_st_Z_in_X_holds_ Z_is_lower let Z be Subset of L; ::_thesis: ( Z in X implies Z is lower ) assume Z in X ; ::_thesis: Z is lower then Z in Ids L by A2; then Z in { Y where Y is Ideal of L : verum } by WAYBEL_0:def_23; then ex Z1 being Ideal of L st Z = Z1 ; hence Z is lower ; ::_thesis: verum end; then reconsider unX = union X as lower Subset of L by A3, WAYBEL_0:26; z in Ids L by A2, A1; then z in { Y where Y is Ideal of L : verum } by WAYBEL_0:def_23; then ex z1 being Ideal of L st z = z1 ; then ex v being set st v in z by XBOOLE_0:def_1; then reconsider unX = unX as non empty lower Subset of L by A1, TARSKI:def_4; A4: now__::_thesis:_for_V,_Y_being_Subset_of_L_st_V_in_X_&_Y_in_X_holds_ ex_Z_being_Subset_of_L_st_ (_Z_in_X_&_V_\/_Y_c=_Z_) let V, Y be Subset of L; ::_thesis: ( V in X & Y in X implies ex Z being Subset of L st ( Z in X & V \/ Y c= Z ) ) assume A5: ( V in X & Y in X ) ; ::_thesis: ex Z being Subset of L st ( Z in X & V \/ Y c= Z ) then reconsider V1 = V, Y1 = Y as Element of (InclPoset (Ids L)) ; consider Z1 being Element of (InclPoset (Ids L)) such that A6: Z1 in X and A7: ( V1 <= Z1 & Y1 <= Z1 ) by A5, WAYBEL_0:def_1; Z1 in Ids L by A2, A6; then Z1 in { Y9 where Y9 is Ideal of L : verum } by WAYBEL_0:def_23; then ex Z2 being Ideal of L st Z1 = Z2 ; then reconsider Z = Z1 as Subset of L ; take Z = Z; ::_thesis: ( Z in X & V \/ Y c= Z ) thus Z in X by A6; ::_thesis: V \/ Y c= Z ( V c= Z & Y c= Z ) by A7, YELLOW_1:3; hence V \/ Y c= Z by XBOOLE_1:8; ::_thesis: verum end; now__::_thesis:_for_Z_being_Subset_of_L_st_Z_in_X_holds_ Z_is_directed let Z be Subset of L; ::_thesis: ( Z in X implies Z is directed ) assume Z in X ; ::_thesis: Z is directed then Z in Ids L by A2; then Z in { Y where Y is Ideal of L : verum } by WAYBEL_0:def_23; then ex Z1 being Ideal of L st Z = Z1 ; hence Z is directed ; ::_thesis: verum end; then reconsider unX = unX as non empty directed lower Subset of L by A3, A4, WAYBEL_0:46; reconsider unX = unX as Element of (InclPoset (Ids L)) by YELLOW_2:41; now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_ Y_c=_sup_X let Y be set ; ::_thesis: ( Y in X implies Y c= sup X ) assume A8: Y in X ; ::_thesis: Y c= sup X then reconsider Y9 = Y as Element of (InclPoset (Ids L)) ; sup X is_>=_than X by YELLOW_0:32; then Y9 <= sup X by A8, LATTICE3:def_9; hence Y c= sup X by YELLOW_1:3; ::_thesis: verum end; then union X c= sup X by ZFMISC_1:76; then A9: unX <= sup X by YELLOW_1:3; now__::_thesis:_for_b_being_Element_of_(InclPoset_(Ids_L))_st_b_in_X_holds_ b_<=_unX let b be Element of (InclPoset (Ids L)); ::_thesis: ( b in X implies b <= unX ) assume b in X ; ::_thesis: b <= unX then b c= union X by ZFMISC_1:74; hence b <= unX by YELLOW_1:3; ::_thesis: verum end; then unX is_>=_than X by LATTICE3:def_9; then sup X <= unX by YELLOW_0:32; hence sup X = union X by A9, ORDERS_2:2; ::_thesis: verum end; theorem Th10: :: WAYBEL13:10 for S being lower-bounded sup-Semilattice holds InclPoset (Ids S) is algebraic proof let S be lower-bounded sup-Semilattice; ::_thesis: InclPoset (Ids S) is algebraic set BS = BoolePoset the carrier of S; Ids S c= bool the carrier of S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ids S or x in bool the carrier of S ) assume x in Ids S ; ::_thesis: x in bool the carrier of S then x in { X where X is Ideal of S : verum } by WAYBEL_0:def_23; then ex x1 being Ideal of S st x = x1 ; hence x in bool the carrier of S ; ::_thesis: verum end; then reconsider InIdsS = InclPoset (Ids S) as non empty full SubRelStr of BoolePoset the carrier of S by YELLOW_1:5; A1: the carrier of InIdsS c= the carrier of (BoolePoset the carrier of S) by YELLOW_0:def_13; now__::_thesis:_for_X_being_Subset_of_InIdsS_st_ex_inf_of_X,_BoolePoset_the_carrier_of_S_holds_ "/\"_(X,(BoolePoset_the_carrier_of_S))_in_the_carrier_of_InIdsS let X be Subset of InIdsS; ::_thesis: ( ex_inf_of X, BoolePoset the carrier of S implies "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS ) assume ex_inf_of X, BoolePoset the carrier of S ; ::_thesis: "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS now__::_thesis:_"/\"_(X,(BoolePoset_the_carrier_of_S))_in_the_carrier_of_InIdsS percases ( X <> {} or X = {} ) ; supposeA2: X <> {} ; ::_thesis: "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS now__::_thesis:_for_x_being_set_st_x_in_X_holds_ x_in_the_carrier_of_(BoolePoset_the_carrier_of_S) let x be set ; ::_thesis: ( x in X implies x in the carrier of (BoolePoset the carrier of S) ) assume x in X ; ::_thesis: x in the carrier of (BoolePoset the carrier of S) then x in the carrier of InIdsS ; hence x in the carrier of (BoolePoset the carrier of S) by A1; ::_thesis: verum end; then X c= the carrier of (BoolePoset the carrier of S) by TARSKI:def_3; then "/\" (X,(BoolePoset the carrier of S)) = meet X by A2, YELLOW_1:20 .= "/\" (X,InIdsS) by A2, YELLOW_2:46 ; hence "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS ; ::_thesis: verum end; supposeA3: X = {} ; ::_thesis: "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS "/\" ({},(BoolePoset the carrier of S)) = Top (BoolePoset the carrier of S) by YELLOW_0:def_12 .= the carrier of S by YELLOW_1:19 .= [#] S .= "/\" ({},InIdsS) by YELLOW_2:47 ; hence "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS by A3; ::_thesis: verum end; end; end; hence "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS ; ::_thesis: verum end; then A4: InIdsS is infs-inheriting by YELLOW_0:def_18; now__::_thesis:_for_Y_being_directed_Subset_of_InIdsS_st_Y_<>_{}_&_ex_sup_of_Y,_BoolePoset_the_carrier_of_S_holds_ "\/"_(Y,(BoolePoset_the_carrier_of_S))_in_the_carrier_of_InIdsS let Y be directed Subset of InIdsS; ::_thesis: ( Y <> {} & ex_sup_of Y, BoolePoset the carrier of S implies "\/" (Y,(BoolePoset the carrier of S)) in the carrier of InIdsS ) assume that A5: Y <> {} and ex_sup_of Y, BoolePoset the carrier of S ; ::_thesis: "\/" (Y,(BoolePoset the carrier of S)) in the carrier of InIdsS now__::_thesis:_for_x_being_set_st_x_in_Y_holds_ x_in_the_carrier_of_(BoolePoset_the_carrier_of_S) let x be set ; ::_thesis: ( x in Y implies x in the carrier of (BoolePoset the carrier of S) ) assume x in Y ; ::_thesis: x in the carrier of (BoolePoset the carrier of S) then x in the carrier of InIdsS ; hence x in the carrier of (BoolePoset the carrier of S) by A1; ::_thesis: verum end; then Y c= the carrier of (BoolePoset the carrier of S) by TARSKI:def_3; then "\/" (Y,(BoolePoset the carrier of S)) = union Y by YELLOW_1:21 .= "\/" (Y,InIdsS) by A5, Th9 ; hence "\/" (Y,(BoolePoset the carrier of S)) in the carrier of InIdsS ; ::_thesis: verum end; then InIdsS is directed-sups-inheriting by WAYBEL_0:def_4; hence InclPoset (Ids S) is algebraic by A4, Th6; ::_thesis: verum end; theorem Th11: :: WAYBEL13:11 for S being lower-bounded sup-Semilattice for x being Element of (InclPoset (Ids S)) holds ( x is compact iff x is principal Ideal of S ) proof let S be lower-bounded sup-Semilattice; ::_thesis: for x being Element of (InclPoset (Ids S)) holds ( x is compact iff x is principal Ideal of S ) reconsider InIdS = InclPoset (Ids S) as CLSubFrame of BoolePoset the carrier of S by Th8; let x be Element of (InclPoset (Ids S)); ::_thesis: ( x is compact iff x is principal Ideal of S ) reconsider x9 = x as Ideal of S by YELLOW_2:41; thus ( x is compact implies x is principal Ideal of S ) ::_thesis: ( x is principal Ideal of S implies x is compact ) proof assume x is compact ; ::_thesis: x is principal Ideal of S then x in the carrier of (CompactSublatt InIdS) by WAYBEL_8:def_1; then consider F being Element of (BoolePoset the carrier of S) such that A1: F is finite and A2: x = meet { Y where Y is Element of InIdS : F c= Y } and A3: F c= x by Th7; A4: F c= the carrier of S by WAYBEL_8:26; ex y being Element of S st ( y in x9 & y is_>=_than x9 ) proof reconsider F9 = F as Subset of S by WAYBEL_8:26; reconsider F9 = F9 as Subset of S ; reconsider y = sup F9 as Element of S ; take y ; ::_thesis: ( y in x9 & y is_>=_than x9 ) now__::_thesis:_y_in_x9 percases ( F9 <> {} or F9 = {} ) ; suppose F9 <> {} ; ::_thesis: y in x9 hence y in x9 by A1, A3, WAYBEL_0:42; ::_thesis: verum end; suppose F9 = {} ; ::_thesis: y in x9 then y = Bottom S by YELLOW_0:def_11; hence y in x9 by WAYBEL_4:21; ::_thesis: verum end; end; end; hence y in x9 ; ::_thesis: y is_>=_than x9 now__::_thesis:_for_b_being_Element_of_S_st_b_in_x9_holds_ b_<=_y now__::_thesis:_for_u_being_set_st_u_in_F_holds_ u_in_downarrow_y let u be set ; ::_thesis: ( u in F implies u in downarrow y ) assume A5: u in F ; ::_thesis: u in downarrow y then reconsider u9 = u as Element of S by A4; ex_sup_of F9,S by A1, A5, YELLOW_0:54; then y is_>=_than F by YELLOW_0:30; then u9 <= y by A5, LATTICE3:def_9; hence u in downarrow y by WAYBEL_0:17; ::_thesis: verum end; then A6: F c= downarrow y by TARSKI:def_3; let b be Element of S; ::_thesis: ( b in x9 implies b <= y ) assume A7: b in x9 ; ::_thesis: b <= y downarrow y is Element of InIdS by YELLOW_2:41; then downarrow y in { Y where Y is Element of InIdS : F c= Y } by A6; then b in downarrow y by A2, A7, SETFAM_1:def_1; hence b <= y by WAYBEL_0:17; ::_thesis: verum end; hence y is_>=_than x9 by LATTICE3:def_9; ::_thesis: verum end; hence x is principal Ideal of S by WAYBEL_0:def_21; ::_thesis: verum end; thus ( x is principal Ideal of S implies x is compact ) ::_thesis: verum proof assume x is principal Ideal of S ; ::_thesis: x is compact then consider y being Element of S such that A8: y in x9 and A9: y is_>=_than x9 by WAYBEL_0:def_21; ex F being Element of (BoolePoset the carrier of S) st ( F is finite & F c= x & x = meet { Y where Y is Element of InIdS : F c= Y } ) proof reconsider F = {y} as Element of (BoolePoset the carrier of S) by WAYBEL_8:26; take F ; ::_thesis: ( F is finite & F c= x & x = meet { Y where Y is Element of InIdS : F c= Y } ) thus F is finite ; ::_thesis: ( F c= x & x = meet { Y where Y is Element of InIdS : F c= Y } ) for v being set st v in F holds v in x by A8, TARSKI:def_1; hence A10: F c= x by TARSKI:def_3; ::_thesis: x = meet { Y where Y is Element of InIdS : F c= Y } A11: now__::_thesis:_for_z_being_set_holds_ (_(_z_in_x_implies_for_Z_being_set_st_Z_in__{__Y_where_Y_is_Element_of_InIdS_:_F_c=_Y__}__holds_ z_in_Z_)_&_(_(_for_Z_being_set_st_Z_in__{__Y_where_Y_is_Element_of_InIdS_:_F_c=_Y__}__holds_ z_in_Z_)_implies_z_in_x_)_) let z be set ; ::_thesis: ( ( z in x implies for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds z in Z ) & ( ( for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds z in Z ) implies z in x ) ) thus ( z in x implies for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds z in Z ) ::_thesis: ( ( for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds z in Z ) implies z in x ) proof assume A12: z in x ; ::_thesis: for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds z in Z then reconsider z9 = z as Element of S by YELLOW_2:42; A13: z9 <= y by A9, A12, LATTICE3:def_9; let Z be set ; ::_thesis: ( Z in { Y where Y is Element of InIdS : F c= Y } implies z in Z ) assume Z in { Y where Y is Element of InIdS : F c= Y } ; ::_thesis: z in Z then consider Z1 being Element of InIdS such that A14: ( Z1 = Z & F c= Z1 ) ; ( Z1 is Ideal of S & y in F ) by TARSKI:def_1, YELLOW_2:41; hence z in Z by A14, A13, WAYBEL_0:def_19; ::_thesis: verum end; thus ( ( for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds z in Z ) implies z in x ) ::_thesis: verum proof assume A15: for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds z in Z ; ::_thesis: z in x x in { Y where Y is Element of InIdS : F c= Y } by A10; hence z in x by A15; ::_thesis: verum end; end; [#] S is Element of InIdS by YELLOW_2:41; then [#] S in { Y where Y is Element of InIdS : F c= Y } ; hence x = meet { Y where Y is Element of InIdS : F c= Y } by A11, SETFAM_1:def_1; ::_thesis: verum end; then x in the carrier of (CompactSublatt InIdS) by Th7; hence x is compact by WAYBEL_8:def_1; ::_thesis: verum end; end; theorem Th12: :: WAYBEL13:12 for S being lower-bounded sup-Semilattice for x being Element of (InclPoset (Ids S)) holds ( x is compact iff ex a being Element of S st x = downarrow a ) proof let S be lower-bounded sup-Semilattice; ::_thesis: for x being Element of (InclPoset (Ids S)) holds ( x is compact iff ex a being Element of S st x = downarrow a ) let x be Element of (InclPoset (Ids S)); ::_thesis: ( x is compact iff ex a being Element of S st x = downarrow a ) thus ( x is compact implies ex a being Element of S st x = downarrow a ) ::_thesis: ( ex a being Element of S st x = downarrow a implies x is compact ) proof assume x is compact ; ::_thesis: ex a being Element of S st x = downarrow a then x is principal Ideal of S by Th11; hence ex a being Element of S st x = downarrow a by WAYBEL_0:48; ::_thesis: verum end; thus ( ex a being Element of S st x = downarrow a implies x is compact ) ::_thesis: verum proof assume ex a being Element of S st x = downarrow a ; ::_thesis: x is compact then x is principal Ideal of S by WAYBEL_0:48; hence x is compact by Th11; ::_thesis: verum end; end; theorem :: WAYBEL13:13 for L being lower-bounded sup-Semilattice for f being Function of L,(CompactSublatt (InclPoset (Ids L))) st ( for x being Element of L holds f . x = downarrow x ) holds f is isomorphic proof let L be lower-bounded sup-Semilattice; ::_thesis: for f being Function of L,(CompactSublatt (InclPoset (Ids L))) st ( for x being Element of L holds f . x = downarrow x ) holds f is isomorphic let f be Function of L,(CompactSublatt (InclPoset (Ids L))); ::_thesis: ( ( for x being Element of L holds f . x = downarrow x ) implies f is isomorphic ) assume A1: for x being Element of L holds f . x = downarrow x ; ::_thesis: f is isomorphic A2: for x, y being Element of L holds ( x <= y iff f . x <= f . y ) proof let x, y be Element of L; ::_thesis: ( x <= y iff f . x <= f . y ) reconsider fx = f . x as Element of (InclPoset (Ids L)) by YELLOW_0:58; reconsider fy = f . y as Element of (InclPoset (Ids L)) by YELLOW_0:58; thus ( x <= y implies f . x <= f . y ) ::_thesis: ( f . x <= f . y implies x <= y ) proof assume x <= y ; ::_thesis: f . x <= f . y then downarrow x c= downarrow y by WAYBEL_0:21; then f . x c= downarrow y by A1; then fx c= fy by A1; then fx <= fy by YELLOW_1:3; hence f . x <= f . y by YELLOW_0:60; ::_thesis: verum end; x <= x ; then A3: x in downarrow x by WAYBEL_0:17; thus ( f . x <= f . y implies x <= y ) ::_thesis: verum proof assume f . x <= f . y ; ::_thesis: x <= y then fx <= fy by YELLOW_0:59; then fx c= fy by YELLOW_1:3; then f . x c= downarrow y by A1; then downarrow x c= downarrow y by A1; hence x <= y by A3, WAYBEL_0:17; ::_thesis: verum end; end; now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_(CompactSublatt_(InclPoset_(Ids_L)))_holds_ ex_x9_being_set_st_ (_x9_in_the_carrier_of_L_&_y_=_f_._x9_) let y be set ; ::_thesis: ( y in the carrier of (CompactSublatt (InclPoset (Ids L))) implies ex x9 being set st ( x9 in the carrier of L & y = f . x9 ) ) assume A4: y in the carrier of (CompactSublatt (InclPoset (Ids L))) ; ::_thesis: ex x9 being set st ( x9 in the carrier of L & y = f . x9 ) the carrier of (CompactSublatt (InclPoset (Ids L))) c= the carrier of (InclPoset (Ids L)) by YELLOW_0:def_13; then reconsider y9 = y as Element of (InclPoset (Ids L)) by A4; y9 is compact by A4, WAYBEL_8:def_1; then consider x being Element of L such that A5: y9 = downarrow x by Th12; reconsider x9 = x as set ; take x9 = x9; ::_thesis: ( x9 in the carrier of L & y = f . x9 ) thus x9 in the carrier of L ; ::_thesis: y = f . x9 thus y = f . x9 by A1, A5; ::_thesis: verum end; then A6: rng f = the carrier of (CompactSublatt (InclPoset (Ids L))) by FUNCT_2:10; now__::_thesis:_for_x,_y_being_Element_of_L_st_f_._x_=_f_._y_holds_ x_=_y let x, y be Element of L; ::_thesis: ( f . x = f . y implies x = y ) assume f . x = f . y ; ::_thesis: x = y then f . x = downarrow y by A1; then downarrow x = downarrow y by A1; hence x = y by WAYBEL_0:19; ::_thesis: verum end; then f is V13() by WAYBEL_1:def_1; hence f is isomorphic by A6, A2, WAYBEL_0:66; ::_thesis: verum end; theorem :: WAYBEL13:14 for S being lower-bounded LATTICE holds InclPoset (Ids S) is arithmetic proof let S be lower-bounded LATTICE; ::_thesis: InclPoset (Ids S) is arithmetic now__::_thesis:_for_x,_y_being_Element_of_(CompactSublatt_(InclPoset_(Ids_S)))_ex_z_being_Element_of_(CompactSublatt_(InclPoset_(Ids_S)))_st_ (_z_<=_x_&_z_<=_y_&_(_for_v_being_Element_of_(CompactSublatt_(InclPoset_(Ids_S)))_st_v_<=_x_&_v_<=_y_holds_ v_<=_z_)_) let x, y be Element of (CompactSublatt (InclPoset (Ids S))); ::_thesis: ex z being Element of (CompactSublatt (InclPoset (Ids S))) st ( z <= x & z <= y & ( for v being Element of (CompactSublatt (InclPoset (Ids S))) st v <= x & v <= y holds v <= z ) ) reconsider x1 = x, y1 = y as Element of (InclPoset (Ids S)) by YELLOW_0:58; x1 is compact by WAYBEL_8:def_1; then consider a being Element of S such that A1: x1 = downarrow a by Th12; y1 is compact by WAYBEL_8:def_1; then consider b being Element of S such that A2: y1 = downarrow b by Th12; Bottom S <= b by YELLOW_0:44; then A3: Bottom S in downarrow b by WAYBEL_0:17; Bottom S <= a by YELLOW_0:44; then Bottom S in downarrow a by WAYBEL_0:17; then reconsider xy = (downarrow a) /\ (downarrow b) as non empty Subset of S by A3, XBOOLE_0:def_4; reconsider xy = xy as non empty lower Subset of S by WAYBEL_0:27; reconsider xy = xy as non empty directed lower Subset of S by WAYBEL_0:44; xy is Ideal of S ; then (downarrow a) /\ (downarrow b) in { X where X is Ideal of S : verum } ; then (downarrow a) /\ (downarrow b) in Ids S by WAYBEL_0:def_23; then x1 "/\" y1 = (downarrow a) /\ (downarrow b) by A1, A2, YELLOW_1:9; then reconsider z1 = (downarrow a) /\ (downarrow b) as Element of (InclPoset (Ids S)) ; z1 c= y1 by A2, XBOOLE_1:17; then A4: z1 <= y1 by YELLOW_1:3; A5: downarrow (a "/\" b) c= (downarrow a) /\ (downarrow b) proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in downarrow (a "/\" b) or v in (downarrow a) /\ (downarrow b) ) assume A6: v in downarrow (a "/\" b) ; ::_thesis: v in (downarrow a) /\ (downarrow b) then reconsider v1 = v as Element of S ; A7: v1 <= a "/\" b by A6, WAYBEL_0:17; a "/\" b <= b by YELLOW_0:23; then v1 <= b by A7, ORDERS_2:3; then A8: v in downarrow b by WAYBEL_0:17; a "/\" b <= a by YELLOW_0:23; then v1 <= a by A7, ORDERS_2:3; then v in downarrow a by WAYBEL_0:17; hence v in (downarrow a) /\ (downarrow b) by A8, XBOOLE_0:def_4; ::_thesis: verum end; (downarrow a) /\ (downarrow b) c= downarrow (a "/\" b) proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in (downarrow a) /\ (downarrow b) or v in downarrow (a "/\" b) ) assume A9: v in (downarrow a) /\ (downarrow b) ; ::_thesis: v in downarrow (a "/\" b) then reconsider v1 = v as Element of S ; v in downarrow b by A9, XBOOLE_0:def_4; then A10: v1 <= b by WAYBEL_0:17; v in downarrow a by A9, XBOOLE_0:def_4; then v1 <= a by WAYBEL_0:17; then v1 <= a "/\" b by A10, YELLOW_0:23; hence v in downarrow (a "/\" b) by WAYBEL_0:17; ::_thesis: verum end; then z1 = downarrow (a "/\" b) by A5, XBOOLE_0:def_10; then z1 is compact by Th12; then reconsider z = z1 as Element of (CompactSublatt (InclPoset (Ids S))) by WAYBEL_8:def_1; take z = z; ::_thesis: ( z <= x & z <= y & ( for v being Element of (CompactSublatt (InclPoset (Ids S))) st v <= x & v <= y holds v <= z ) ) z1 c= x1 by A1, XBOOLE_1:17; then z1 <= x1 by YELLOW_1:3; hence ( z <= x & z <= y ) by A4, YELLOW_0:60; ::_thesis: for v being Element of (CompactSublatt (InclPoset (Ids S))) st v <= x & v <= y holds v <= z let v be Element of (CompactSublatt (InclPoset (Ids S))); ::_thesis: ( v <= x & v <= y implies v <= z ) reconsider v1 = v as Element of (InclPoset (Ids S)) by YELLOW_0:58; assume that A11: v <= x and A12: v <= y ; ::_thesis: v <= z v1 <= y1 by A12, YELLOW_0:59; then A13: v1 c= y1 by YELLOW_1:3; v1 <= x1 by A11, YELLOW_0:59; then v1 c= x1 by YELLOW_1:3; then v1 c= z1 by A1, A2, A13, XBOOLE_1:19; then v1 <= z1 by YELLOW_1:3; hence v <= z by YELLOW_0:60; ::_thesis: verum end; then A14: CompactSublatt (InclPoset (Ids S)) is with_infima by LATTICE3:def_11; InclPoset (Ids S) is algebraic by Th10; hence InclPoset (Ids S) is arithmetic by A14, WAYBEL_8:19; ::_thesis: verum end; theorem Th15: :: WAYBEL13:15 for L being lower-bounded sup-Semilattice holds CompactSublatt L is lower-bounded sup-Semilattice proof let L be lower-bounded sup-Semilattice; ::_thesis: CompactSublatt L is lower-bounded sup-Semilattice ex x being Element of (CompactSublatt L) st x is_<=_than the carrier of (CompactSublatt L) proof reconsider x = Bottom L as Element of (CompactSublatt L) by WAYBEL_8:3; take x ; ::_thesis: x is_<=_than the carrier of (CompactSublatt L) now__::_thesis:_for_a_being_Element_of_(CompactSublatt_L)_st_a_in_the_carrier_of_(CompactSublatt_L)_holds_ x_<=_a let a be Element of (CompactSublatt L); ::_thesis: ( a in the carrier of (CompactSublatt L) implies x <= a ) A1: the carrier of (CompactSublatt L) c= the carrier of L by YELLOW_0:def_13; assume a in the carrier of (CompactSublatt L) ; ::_thesis: x <= a then reconsider a9 = a as Element of L by A1; Bottom L <= a9 by YELLOW_0:44; hence x <= a by YELLOW_0:60; ::_thesis: verum end; hence x is_<=_than the carrier of (CompactSublatt L) by LATTICE3:def_8; ::_thesis: verum end; hence CompactSublatt L is lower-bounded sup-Semilattice by YELLOW_0:def_4; ::_thesis: verum end; theorem Th16: :: WAYBEL13:16 for L being lower-bounded algebraic sup-Semilattice for f being Function of L,(InclPoset (Ids (CompactSublatt L))) st ( for x being Element of L holds f . x = compactbelow x ) holds f is isomorphic proof let L be lower-bounded algebraic sup-Semilattice; ::_thesis: for f being Function of L,(InclPoset (Ids (CompactSublatt L))) st ( for x being Element of L holds f . x = compactbelow x ) holds f is isomorphic let f be Function of L,(InclPoset (Ids (CompactSublatt L))); ::_thesis: ( ( for x being Element of L holds f . x = compactbelow x ) implies f is isomorphic ) assume A1: for x being Element of L holds f . x = compactbelow x ; ::_thesis: f is isomorphic A2: now__::_thesis:_for_x,_y_being_Element_of_L_holds_ (_(_x_<=_y_implies_f_._x_<=_f_._y_)_&_(_f_._x_<=_f_._y_implies_x_<=_y_)_) let x, y be Element of L; ::_thesis: ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) ) thus ( x <= y implies f . x <= f . y ) ::_thesis: ( f . x <= f . y implies x <= y ) proof assume x <= y ; ::_thesis: f . x <= f . y then compactbelow x c= compactbelow y by Th1; then f . x c= compactbelow y by A1; then f . x c= f . y by A1; hence f . x <= f . y by YELLOW_1:3; ::_thesis: verum end; thus ( f . x <= f . y implies x <= y ) ::_thesis: verum proof assume f . x <= f . y ; ::_thesis: x <= y then f . x c= f . y by YELLOW_1:3; then f . x c= compactbelow y by A1; then A3: compactbelow x c= compactbelow y by A1; ( ex_sup_of compactbelow x,L & ex_sup_of compactbelow y,L ) by YELLOW_0:17; then sup (compactbelow x) <= sup (compactbelow y) by A3, YELLOW_0:34; then sup (compactbelow x) <= y by WAYBEL_8:def_3; hence x <= y by WAYBEL_8:def_3; ::_thesis: verum end; end; now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_(InclPoset_(Ids_(CompactSublatt_L)))_holds_ ex_x9_being_set_st_ (_x9_in_the_carrier_of_L_&_y_=_f_._x9_) let y be set ; ::_thesis: ( y in the carrier of (InclPoset (Ids (CompactSublatt L))) implies ex x9 being set st ( x9 in the carrier of L & y = f . x9 ) ) assume y in the carrier of (InclPoset (Ids (CompactSublatt L))) ; ::_thesis: ex x9 being set st ( x9 in the carrier of L & y = f . x9 ) then reconsider y9 = y as Ideal of (CompactSublatt L) by YELLOW_2:41; reconsider y1 = y9 as non empty Subset of L by Th3; reconsider y1 = y1 as non empty directed Subset of L by YELLOW_2:7; set x = sup y1; reconsider x9 = sup y1 as set ; take x9 = x9; ::_thesis: ( x9 in the carrier of L & y = f . x9 ) thus x9 in the carrier of L ; ::_thesis: y = f . x9 A4: compactbelow (sup y1) c= y9 proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in compactbelow (sup y1) or d in y9 ) assume d in compactbelow (sup y1) ; ::_thesis: d in y9 then d in { v where v is Element of L : ( sup y1 >= v & v is compact ) } by WAYBEL_8:def_2; then consider d1 being Element of L such that A5: d1 = d and A6: d1 <= sup y1 and A7: d1 is compact ; reconsider d9 = d1 as Element of (CompactSublatt L) by A7, WAYBEL_8:def_1; d1 << d1 by A7, WAYBEL_3:def_2; then consider z being Element of L such that A8: z in y1 and A9: d1 <= z by A6, WAYBEL_3:def_1; reconsider z9 = z as Element of (CompactSublatt L) by A8; d9 <= z9 by A9, YELLOW_0:60; hence d in y9 by A5, A8, WAYBEL_0:def_19; ::_thesis: verum end; y9 c= compactbelow (sup y1) proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in y9 or d in compactbelow (sup y1) ) assume A10: d in y9 ; ::_thesis: d in compactbelow (sup y1) then reconsider d1 = d as Element of (CompactSublatt L) ; reconsider d9 = d1 as Element of L by YELLOW_0:58; y9 is_<=_than sup y1 by YELLOW_0:32; then ( d9 is compact & d9 <= sup y1 ) by A10, LATTICE3:def_9, WAYBEL_8:def_1; hence d in compactbelow (sup y1) by WAYBEL_8:4; ::_thesis: verum end; hence y = compactbelow (sup y1) by A4, XBOOLE_0:def_10 .= f . x9 by A1 ; ::_thesis: verum end; then A11: rng f = the carrier of (InclPoset (Ids (CompactSublatt L))) by FUNCT_2:10; now__::_thesis:_for_x,_y_being_Element_of_L_st_f_._x_=_f_._y_holds_ x_=_y let x, y be Element of L; ::_thesis: ( f . x = f . y implies x = y ) assume f . x = f . y ; ::_thesis: x = y then f . x = compactbelow y by A1; then compactbelow x = compactbelow y by A1; then sup (compactbelow x) = y by WAYBEL_8:def_3; hence x = y by WAYBEL_8:def_3; ::_thesis: verum end; then f is V13() by WAYBEL_1:def_1; hence f is isomorphic by A11, A2, WAYBEL_0:66; ::_thesis: verum end; theorem :: WAYBEL13:17 for L being lower-bounded algebraic sup-Semilattice for x being Element of L holds ( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact ) proof let L be lower-bounded algebraic sup-Semilattice; ::_thesis: for x being Element of L holds ( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact ) let x be Element of L; ::_thesis: ( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact ) thus ( compactbelow x is principal Ideal of (CompactSublatt L) implies x is compact ) ::_thesis: ( x is compact implies compactbelow x is principal Ideal of (CompactSublatt L) ) proof assume compactbelow x is principal Ideal of (CompactSublatt L) ; ::_thesis: x is compact then consider y being Element of (CompactSublatt L) such that A1: y in compactbelow x and A2: y is_>=_than compactbelow x by WAYBEL_0:def_21; reconsider y9 = y as Element of L by YELLOW_0:58; compactbelow x is Subset of (CompactSublatt L) by Th2; then y9 is_>=_than compactbelow x by A2, YELLOW_0:62; then y9 >= sup (compactbelow x) by YELLOW_0:32; then A3: x <= y9 by WAYBEL_8:def_3; ( y9 <= x & y9 is compact ) by A1, WAYBEL_8:4; hence x is compact by A3, ORDERS_2:2; ::_thesis: verum end; thus ( x is compact implies compactbelow x is principal Ideal of (CompactSublatt L) ) ::_thesis: verum proof reconsider I = compactbelow x as non empty Subset of (CompactSublatt L) by Th2; assume A4: x is compact ; ::_thesis: compactbelow x is principal Ideal of (CompactSublatt L) then reconsider x9 = x as Element of (CompactSublatt L) by WAYBEL_8:def_1; compactbelow x is non empty directed Subset of L by WAYBEL_8:def_4; then reconsider I = I as non empty directed Subset of (CompactSublatt L) by WAYBEL10:23; now__::_thesis:_for_y,_z_being_Element_of_(CompactSublatt_L)_st_y_in_I_&_z_<=_y_holds_ z_in_I let y, z be Element of (CompactSublatt L); ::_thesis: ( y in I & z <= y implies z in I ) reconsider y9 = y, z9 = z as Element of L by YELLOW_0:58; assume ( y in I & z <= y ) ; ::_thesis: z in I then ( y9 <= x & z9 <= y9 ) by WAYBEL_8:4, YELLOW_0:59; then A5: z9 <= x by ORDERS_2:3; z9 is compact by WAYBEL_8:def_1; hence z in I by A5, WAYBEL_8:4; ::_thesis: verum end; then reconsider I = I as Ideal of (CompactSublatt L) by WAYBEL_0:def_19; sup (compactbelow x) is_>=_than compactbelow x by YELLOW_0:32; then x is_>=_than I by WAYBEL_8:def_3; then A6: x9 is_>=_than I by YELLOW_0:61; x <= x ; then x9 in I by A4, WAYBEL_8:4; hence compactbelow x is principal Ideal of (CompactSublatt L) by A6, WAYBEL_0:def_21; ::_thesis: verum end; end; begin theorem Th18: :: WAYBEL13:18 for L1, L2 being non empty RelStr for X being Subset of L1 for x being Element of L1 for f being Function of L1,L2 st f is isomorphic holds ( x is_<=_than X iff f . x is_<=_than f .: X ) proof let L1, L2 be non empty RelStr ; ::_thesis: for X being Subset of L1 for x being Element of L1 for f being Function of L1,L2 st f is isomorphic holds ( x is_<=_than X iff f . x is_<=_than f .: X ) let X be Subset of L1; ::_thesis: for x being Element of L1 for f being Function of L1,L2 st f is isomorphic holds ( x is_<=_than X iff f . x is_<=_than f .: X ) let x be Element of L1; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds ( x is_<=_than X iff f . x is_<=_than f .: X ) let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies ( x is_<=_than X iff f . x is_<=_than f .: X ) ) assume A1: f is isomorphic ; ::_thesis: ( x is_<=_than X iff f . x is_<=_than f .: X ) hence ( x is_<=_than X implies f . x is_<=_than f .: X ) by YELLOW_2:13; ::_thesis: ( f . x is_<=_than f .: X implies x is_<=_than X ) thus ( f . x is_<=_than f .: X implies x is_<=_than X ) ::_thesis: verum proof reconsider g = f " as Function of L2,L1 by A1, WAYBEL_0:67; assume A2: f . x is_<=_than f .: X ; ::_thesis: x is_<=_than X g is isomorphic by A1, WAYBEL_0:68; then A3: g . (f . x) is_<=_than g .: (f .: X) by A2, YELLOW_2:13; A4: f " (f .: X) c= X by A1, FUNCT_1:82; X c= the carrier of L1 ; then X c= dom f by FUNCT_2:def_1; then A5: X c= f " (f .: X) by FUNCT_1:76; x in the carrier of L1 ; then A6: x in dom f by FUNCT_2:def_1; g .: (f .: X) = f " (f .: X) by A1, FUNCT_1:85 .= X by A4, A5, XBOOLE_0:def_10 ; hence x is_<=_than X by A1, A6, A3, FUNCT_1:34; ::_thesis: verum end; end; theorem Th19: :: WAYBEL13:19 for L1, L2 being non empty RelStr for X being Subset of L1 for x being Element of L1 for f being Function of L1,L2 st f is isomorphic holds ( x is_>=_than X iff f . x is_>=_than f .: X ) proof let L1, L2 be non empty RelStr ; ::_thesis: for X being Subset of L1 for x being Element of L1 for f being Function of L1,L2 st f is isomorphic holds ( x is_>=_than X iff f . x is_>=_than f .: X ) let X be Subset of L1; ::_thesis: for x being Element of L1 for f being Function of L1,L2 st f is isomorphic holds ( x is_>=_than X iff f . x is_>=_than f .: X ) let x be Element of L1; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds ( x is_>=_than X iff f . x is_>=_than f .: X ) let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies ( x is_>=_than X iff f . x is_>=_than f .: X ) ) assume A1: f is isomorphic ; ::_thesis: ( x is_>=_than X iff f . x is_>=_than f .: X ) hence ( x is_>=_than X implies f . x is_>=_than f .: X ) by YELLOW_2:14; ::_thesis: ( f . x is_>=_than f .: X implies x is_>=_than X ) thus ( f . x is_>=_than f .: X implies x is_>=_than X ) ::_thesis: verum proof reconsider g = f " as Function of L2,L1 by A1, WAYBEL_0:67; assume A2: f . x is_>=_than f .: X ; ::_thesis: x is_>=_than X g is isomorphic by A1, WAYBEL_0:68; then A3: g . (f . x) is_>=_than g .: (f .: X) by A2, YELLOW_2:14; A4: f " (f .: X) c= X by A1, FUNCT_1:82; X c= the carrier of L1 ; then X c= dom f by FUNCT_2:def_1; then A5: X c= f " (f .: X) by FUNCT_1:76; x in the carrier of L1 ; then A6: x in dom f by FUNCT_2:def_1; g .: (f .: X) = f " (f .: X) by A1, FUNCT_1:85 .= X by A4, A5, XBOOLE_0:def_10 ; hence x is_>=_than X by A1, A6, A3, FUNCT_1:34; ::_thesis: verum end; end; theorem Th20: :: WAYBEL13:20 for L1, L2 being non empty antisymmetric RelStr for f being Function of L1,L2 st f is isomorphic holds ( f is infs-preserving & f is sups-preserving ) proof let L1, L2 be non empty antisymmetric RelStr ; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds ( f is infs-preserving & f is sups-preserving ) let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies ( f is infs-preserving & f is sups-preserving ) ) assume A1: f is isomorphic ; ::_thesis: ( f is infs-preserving & f is sups-preserving ) then A2: rng f = the carrier of L2 by WAYBEL_0:66; now__::_thesis:_for_X_being_Subset_of_L1_holds_f_preserves_inf_of_X let X be Subset of L1; ::_thesis: f preserves_inf_of X now__::_thesis:_(_ex_inf_of_X,L1_implies_(_ex_inf_of_f_.:_X,L2_&_inf_(f_.:_X)_=_f_._(inf_X)_)_) assume A3: ex_inf_of X,L1 ; ::_thesis: ( ex_inf_of f .: X,L2 & inf (f .: X) = f . (inf X) ) then consider a being Element of L1 such that A4: X is_>=_than a and A5: for b being Element of L1 st X is_>=_than b holds a >= b by YELLOW_0:16; A6: now__::_thesis:_for_c_being_Element_of_L2_st_f_.:_X_is_>=_than_c_holds_ f_._a_>=_c let c be Element of L2; ::_thesis: ( f .: X is_>=_than c implies f . a >= c ) consider e being set such that A7: e in dom f and A8: c = f . e by A2, FUNCT_1:def_3; reconsider e = e as Element of L1 by A7; assume f .: X is_>=_than c ; ::_thesis: f . a >= c then X is_>=_than e by A1, A8, Th18; then a >= e by A5; hence f . a >= c by A1, A8, WAYBEL_0:66; ::_thesis: verum end; f .: X is_>=_than f . a by A1, A4, Th18; hence ex_inf_of f .: X,L2 by A6, YELLOW_0:16; ::_thesis: inf (f .: X) = f . (inf X) A9: now__::_thesis:_for_b_being_Element_of_L2_st_b_is_<=_than_f_.:_X_holds_ f_._(inf_X)_>=_b let b be Element of L2; ::_thesis: ( b is_<=_than f .: X implies f . (inf X) >= b ) consider v being set such that A10: v in dom f and A11: b = f . v by A2, FUNCT_1:def_3; reconsider v = v as Element of L1 by A10; assume b is_<=_than f .: X ; ::_thesis: f . (inf X) >= b then v is_<=_than X by A1, A11, Th18; then inf X >= v by A3, YELLOW_0:31; hence f . (inf X) >= b by A1, A11, WAYBEL_0:66; ::_thesis: verum end; inf X is_<=_than X by A3, YELLOW_0:31; then f . (inf X) is_<=_than f .: X by A1, Th18; hence inf (f .: X) = f . (inf X) by A9, YELLOW_0:31; ::_thesis: verum end; hence f preserves_inf_of X by WAYBEL_0:def_30; ::_thesis: verum end; hence f is infs-preserving by WAYBEL_0:def_32; ::_thesis: f is sups-preserving now__::_thesis:_for_X_being_Subset_of_L1_holds_f_preserves_sup_of_X let X be Subset of L1; ::_thesis: f preserves_sup_of X now__::_thesis:_(_ex_sup_of_X,L1_implies_(_ex_sup_of_f_.:_X,L2_&_sup_(f_.:_X)_=_f_._(sup_X)_)_) assume A12: ex_sup_of X,L1 ; ::_thesis: ( ex_sup_of f .: X,L2 & sup (f .: X) = f . (sup X) ) then consider a being Element of L1 such that A13: X is_<=_than a and A14: for b being Element of L1 st X is_<=_than b holds a <= b by YELLOW_0:15; A15: now__::_thesis:_for_c_being_Element_of_L2_st_f_.:_X_is_<=_than_c_holds_ f_._a_<=_c let c be Element of L2; ::_thesis: ( f .: X is_<=_than c implies f . a <= c ) consider e being set such that A16: e in dom f and A17: c = f . e by A2, FUNCT_1:def_3; reconsider e = e as Element of L1 by A16; assume f .: X is_<=_than c ; ::_thesis: f . a <= c then X is_<=_than e by A1, A17, Th19; then a <= e by A14; hence f . a <= c by A1, A17, WAYBEL_0:66; ::_thesis: verum end; f .: X is_<=_than f . a by A1, A13, Th19; hence ex_sup_of f .: X,L2 by A15, YELLOW_0:15; ::_thesis: sup (f .: X) = f . (sup X) A18: now__::_thesis:_for_b_being_Element_of_L2_st_b_is_>=_than_f_.:_X_holds_ f_._(sup_X)_<=_b let b be Element of L2; ::_thesis: ( b is_>=_than f .: X implies f . (sup X) <= b ) consider v being set such that A19: v in dom f and A20: b = f . v by A2, FUNCT_1:def_3; reconsider v = v as Element of L1 by A19; assume b is_>=_than f .: X ; ::_thesis: f . (sup X) <= b then v is_>=_than X by A1, A20, Th19; then sup X <= v by A12, YELLOW_0:30; hence f . (sup X) <= b by A1, A20, WAYBEL_0:66; ::_thesis: verum end; sup X is_>=_than X by A12, YELLOW_0:30; then f . (sup X) is_>=_than f .: X by A1, Th19; hence sup (f .: X) = f . (sup X) by A18, YELLOW_0:30; ::_thesis: verum end; hence f preserves_sup_of X by WAYBEL_0:def_31; ::_thesis: verum end; hence f is sups-preserving by WAYBEL_0:def_33; ::_thesis: verum end; registration let L1, L2 be non empty antisymmetric RelStr ; cluster Function-like V21( the carrier of L1, the carrier of L2) isomorphic -> infs-preserving sups-preserving for Element of K32(K33( the carrier of L1, the carrier of L2)); coherence for b1 being Function of L1,L2 st b1 is isomorphic holds ( b1 is infs-preserving & b1 is sups-preserving ) by Th20; end; theorem Th21: :: WAYBEL13:21 for L1, L2, L3 being non empty transitive antisymmetric RelStr for f being Function of L1,L2 st f is infs-preserving & L2 is full infs-inheriting SubRelStr of L3 & L3 is complete holds ex g being Function of L1,L3 st ( f = g & g is infs-preserving ) proof let L1, L2, L3 be non empty transitive antisymmetric RelStr ; ::_thesis: for f being Function of L1,L2 st f is infs-preserving & L2 is full infs-inheriting SubRelStr of L3 & L3 is complete holds ex g being Function of L1,L3 st ( f = g & g is infs-preserving ) let f be Function of L1,L2; ::_thesis: ( f is infs-preserving & L2 is full infs-inheriting SubRelStr of L3 & L3 is complete implies ex g being Function of L1,L3 st ( f = g & g is infs-preserving ) ) assume that A1: f is infs-preserving and A2: L2 is full infs-inheriting SubRelStr of L3 and A3: L3 is complete ; ::_thesis: ex g being Function of L1,L3 st ( f = g & g is infs-preserving ) the carrier of L2 c= the carrier of L3 by A2, YELLOW_0:def_13; then reconsider g = f as Function of L1,L3 by FUNCT_2:7; take g ; ::_thesis: ( f = g & g is infs-preserving ) thus f = g ; ::_thesis: g is infs-preserving now__::_thesis:_for_X_being_Subset_of_L1_holds_g_preserves_inf_of_X let X be Subset of L1; ::_thesis: g preserves_inf_of X now__::_thesis:_(_ex_inf_of_X,L1_implies_(_ex_inf_of_g_.:_X,L3_&_inf_(g_.:_X)_=_g_._(inf_X)_)_) A4: f preserves_inf_of X by A1, WAYBEL_0:def_32; assume A5: ex_inf_of X,L1 ; ::_thesis: ( ex_inf_of g .: X,L3 & inf (g .: X) = g . (inf X) ) thus A6: ex_inf_of g .: X,L3 by A3, YELLOW_0:17; ::_thesis: inf (g .: X) = g . (inf X) then "/\" ((f .: X),L3) in the carrier of L2 by A2, YELLOW_0:def_18; hence inf (g .: X) = inf (f .: X) by A2, A6, YELLOW_0:63 .= g . (inf X) by A5, A4, WAYBEL_0:def_30 ; ::_thesis: verum end; hence g preserves_inf_of X by WAYBEL_0:def_30; ::_thesis: verum end; hence g is infs-preserving by WAYBEL_0:def_32; ::_thesis: verum end; theorem Th22: :: WAYBEL13:22 for L1, L2, L3 being non empty transitive antisymmetric RelStr for f being Function of L1,L2 st f is monotone & f is directed-sups-preserving & L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete holds ex g being Function of L1,L3 st ( f = g & g is directed-sups-preserving ) proof let L1, L2, L3 be non empty transitive antisymmetric RelStr ; ::_thesis: for f being Function of L1,L2 st f is monotone & f is directed-sups-preserving & L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete holds ex g being Function of L1,L3 st ( f = g & g is directed-sups-preserving ) let f be Function of L1,L2; ::_thesis: ( f is monotone & f is directed-sups-preserving & L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete implies ex g being Function of L1,L3 st ( f = g & g is directed-sups-preserving ) ) assume that A1: ( f is monotone & f is directed-sups-preserving ) and A2: L2 is full directed-sups-inheriting SubRelStr of L3 and A3: L3 is complete ; ::_thesis: ex g being Function of L1,L3 st ( f = g & g is directed-sups-preserving ) the carrier of L2 c= the carrier of L3 by A2, YELLOW_0:def_13; then reconsider g = f as Function of L1,L3 by FUNCT_2:7; take g ; ::_thesis: ( f = g & g is directed-sups-preserving ) thus f = g ; ::_thesis: g is directed-sups-preserving now__::_thesis:_for_X_being_Subset_of_L1_st_not_X_is_empty_&_X_is_directed_holds_ g_preserves_sup_of_X let X be Subset of L1; ::_thesis: ( not X is empty & X is directed implies g preserves_sup_of X ) assume A4: ( not X is empty & X is directed ) ; ::_thesis: g preserves_sup_of X then consider d being set such that A5: d in X by XBOOLE_0:def_1; d in the carrier of L1 by A5; then d in dom f by FUNCT_2:def_1; then f . d in f .: X by A5, FUNCT_1:def_6; then A6: ( not f .: X is empty & f .: X is directed ) by A1, A4, YELLOW_2:15; now__::_thesis:_(_ex_sup_of_X,L1_implies_(_ex_sup_of_g_.:_X,L3_&_sup_(g_.:_X)_=_g_._(sup_X)_)_) A7: f preserves_sup_of X by A1, A4, WAYBEL_0:def_37; assume A8: ex_sup_of X,L1 ; ::_thesis: ( ex_sup_of g .: X,L3 & sup (g .: X) = g . (sup X) ) thus ex_sup_of g .: X,L3 by A3, YELLOW_0:17; ::_thesis: sup (g .: X) = g . (sup X) hence sup (g .: X) = sup (f .: X) by A2, A6, WAYBEL_0:7 .= g . (sup X) by A8, A7, WAYBEL_0:def_31 ; ::_thesis: verum end; hence g preserves_sup_of X by WAYBEL_0:def_31; ::_thesis: verum end; hence g is directed-sups-preserving by WAYBEL_0:def_37; ::_thesis: verum end; theorem Th23: :: WAYBEL13:23 for L being lower-bounded sup-Semilattice holds InclPoset (Ids (CompactSublatt L)) is CLSubFrame of BoolePoset the carrier of (CompactSublatt L) proof let L be lower-bounded sup-Semilattice; ::_thesis: InclPoset (Ids (CompactSublatt L)) is CLSubFrame of BoolePoset the carrier of (CompactSublatt L) CompactSublatt L is lower-bounded sup-Semilattice by Th15; hence InclPoset (Ids (CompactSublatt L)) is CLSubFrame of BoolePoset the carrier of (CompactSublatt L) by Th8; ::_thesis: verum end; theorem Th24: :: WAYBEL13:24 for L being lower-bounded algebraic LATTICE ex g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st ( g is infs-preserving & g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) ) proof let L be lower-bounded algebraic LATTICE; ::_thesis: ex g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st ( g is infs-preserving & g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) ) deffunc H1( Element of L) -> Element of K32( the carrier of L) = compactbelow $1; A1: for y being Element of L holds H1(y) is Element of (InclPoset (Ids (CompactSublatt L))) proof let y be Element of L; ::_thesis: H1(y) is Element of (InclPoset (Ids (CompactSublatt L))) reconsider comy = compactbelow y as non empty directed Subset of L by WAYBEL_8:def_4; reconsider comy = comy as non empty Subset of (CompactSublatt L) by Th2; reconsider comy = comy as non empty directed Subset of (CompactSublatt L) by WAYBEL10:23; now__::_thesis:_for_x1,_z1_being_Element_of_(CompactSublatt_L)_st_x1_in_comy_&_z1_<=_x1_holds_ z1_in_comy let x1, z1 be Element of (CompactSublatt L); ::_thesis: ( x1 in comy & z1 <= x1 implies z1 in comy ) reconsider x2 = x1, z2 = z1 as Element of L by YELLOW_0:58; assume ( x1 in comy & z1 <= x1 ) ; ::_thesis: z1 in comy then ( x2 <= y & z2 <= x2 ) by WAYBEL_8:4, YELLOW_0:59; then A2: z2 <= y by ORDERS_2:3; z2 is compact by WAYBEL_8:def_1; hence z1 in comy by A2, WAYBEL_8:4; ::_thesis: verum end; then comy is lower by WAYBEL_0:def_19; hence H1(y) is Element of (InclPoset (Ids (CompactSublatt L))) by YELLOW_2:41; ::_thesis: verum end; consider g1 being Function of L,(InclPoset (Ids (CompactSublatt L))) such that A3: for y being Element of L holds g1 . y = H1(y) from FUNCT_2:sch_9(A1); now__::_thesis:_for_k_being_set_st_k_in_the_carrier_of_(InclPoset_(Ids_(CompactSublatt_L)))_holds_ k_in_the_carrier_of_(BoolePoset_the_carrier_of_(CompactSublatt_L)) let k be set ; ::_thesis: ( k in the carrier of (InclPoset (Ids (CompactSublatt L))) implies k in the carrier of (BoolePoset the carrier of (CompactSublatt L)) ) assume k in the carrier of (InclPoset (Ids (CompactSublatt L))) ; ::_thesis: k in the carrier of (BoolePoset the carrier of (CompactSublatt L)) then k is Ideal of (CompactSublatt L) by YELLOW_2:41; then k is Element of (BoolePoset the carrier of (CompactSublatt L)) by WAYBEL_8:26; hence k in the carrier of (BoolePoset the carrier of (CompactSublatt L)) ; ::_thesis: verum end; then the carrier of (InclPoset (Ids (CompactSublatt L))) c= the carrier of (BoolePoset the carrier of (CompactSublatt L)) by TARSKI:def_3; then reconsider g = g1 as Function of L,(BoolePoset the carrier of (CompactSublatt L)) by FUNCT_2:7; take g ; ::_thesis: ( g is infs-preserving & g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) ) A4: g1 is isomorphic by A3, Th16; A5: InclPoset (Ids (CompactSublatt L)) is full infs-inheriting directed-sups-inheriting SubRelStr of BoolePoset the carrier of (CompactSublatt L) by Th23; then ex g2 being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st ( g1 = g2 & g2 is infs-preserving ) by A4, Th21; hence g is infs-preserving ; ::_thesis: ( g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) ) ex g3 being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st ( g1 = g3 & g3 is directed-sups-preserving ) by A4, A5, Th22; hence g is directed-sups-preserving ; ::_thesis: ( g is V13() & ( for x being Element of L holds g . x = compactbelow x ) ) thus g is V13() by A4; ::_thesis: for x being Element of L holds g . x = compactbelow x let x be Element of L; ::_thesis: g . x = compactbelow x thus g . x = compactbelow x by A3; ::_thesis: verum end; theorem :: WAYBEL13:25 for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is lower-bounded algebraic LATTICE ) holds product J is lower-bounded algebraic LATTICE proof let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is lower-bounded algebraic LATTICE ) holds product J is lower-bounded algebraic LATTICE let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is lower-bounded algebraic LATTICE ) implies product J is lower-bounded algebraic LATTICE ) assume A1: for i being Element of I holds J . i is lower-bounded algebraic LATTICE ; ::_thesis: product J is lower-bounded algebraic LATTICE then A2: for i being Element of I holds J . i is complete LATTICE ; then reconsider L = product J as non empty lower-bounded LATTICE by WAYBEL_3:31; for i being Element of I holds J . i is antisymmetric by A1; then A3: product J is antisymmetric by WAYBEL_3:30; now__::_thesis:_for_x_being_Element_of_(product_J)_holds_x_=_sup_(compactbelow_x) let x be Element of (product J); ::_thesis: x = sup (compactbelow x) A4: for i being Element of I holds sup (compactbelow (x . i)) = (sup (compactbelow x)) . i proof let i be Element of I; ::_thesis: sup (compactbelow (x . i)) = (sup (compactbelow x)) . i A5: compactbelow (x . i) c= pi ((compactbelow x),i) proof deffunc H1( Element of I) -> Element of the carrier of (J . $1) = Bottom (J . $1); defpred S1[ set ] means $1 = i; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in compactbelow (x . i) or v in pi ((compactbelow x),i) ) assume v in compactbelow (x . i) ; ::_thesis: v in pi ((compactbelow x),i) then v in { y where y is Element of (J . i) : ( x . i >= y & y is compact ) } by WAYBEL_8:def_2; then consider v1 being Element of (J . i) such that A6: v1 = v and A7: x . i >= v1 and A8: v1 is compact ; deffunc H2( set ) -> Element of (J . i) = v1; consider f being Function such that A9: dom f = I and A10: for j being Element of I holds ( ( S1[j] implies f . j = H2(j) ) & ( not S1[j] implies f . j = H1(j) ) ) from PARTFUN1:sch_4(); A11: f . i = v1 by A10; now__::_thesis:_for_k_being_Element_of_I_holds_f_._k_is_Element_of_(J_._k) let k be Element of I; ::_thesis: f . k is Element of (J . k) now__::_thesis:_f_._k_is_Element_of_(J_._k) percases ( k = i or k <> i ) ; suppose k = i ; ::_thesis: f . k is Element of (J . k) hence f . k is Element of (J . k) by A10; ::_thesis: verum end; suppose k <> i ; ::_thesis: f . k is Element of (J . k) then f . k = Bottom (J . k) by A10; hence f . k is Element of (J . k) ; ::_thesis: verum end; end; end; hence f . k is Element of (J . k) ; ::_thesis: verum end; then reconsider f = f as Element of (product J) by A9, WAYBEL_3:27; now__::_thesis:_for_k_being_Element_of_I_holds_f_._k_<=_x_._k let k be Element of I; ::_thesis: f . k <= x . k A12: J . k is lower-bounded algebraic LATTICE by A1; now__::_thesis:_f_._k_<=_x_._k percases ( k = i or k <> i ) ; suppose k = i ; ::_thesis: f . k <= x . k hence f . k <= x . k by A7, A10; ::_thesis: verum end; suppose k <> i ; ::_thesis: f . k <= x . k then f . k = Bottom (J . k) by A10; hence f . k <= x . k by A12, YELLOW_0:44; ::_thesis: verum end; end; end; hence f . k <= x . k ; ::_thesis: verum end; then A13: f <= x by WAYBEL_3:28; A14: now__::_thesis:_for_k_being_Element_of_I_holds_f_._k_<<_f_._k let k be Element of I; ::_thesis: f . k << f . k A15: J . k is lower-bounded algebraic LATTICE by A1; now__::_thesis:_f_._k_<<_f_._k percases ( k = i or k <> i ) ; supposeA16: k = i ; ::_thesis: f . k << f . k then f . k = v1 by A10; hence f . k << f . k by A8, A16, WAYBEL_3:def_2; ::_thesis: verum end; suppose k <> i ; ::_thesis: f . k << f . k then f . k = Bottom (J . k) by A10; then f . k is compact by A15, WAYBEL_3:15; hence f . k << f . k by WAYBEL_3:def_2; ::_thesis: verum end; end; end; hence f . k << f . k ; ::_thesis: verum end; ex K being finite Subset of I st for k being Element of I st not k in K holds f . k = Bottom (J . k) proof take K = {i}; ::_thesis: for k being Element of I st not k in K holds f . k = Bottom (J . k) let k be Element of I; ::_thesis: ( not k in K implies f . k = Bottom (J . k) ) assume not k in K ; ::_thesis: f . k = Bottom (J . k) then k <> i by TARSKI:def_1; hence f . k = Bottom (J . k) by A10; ::_thesis: verum end; then f << f by A2, A14, WAYBEL_3:33; then f is compact by WAYBEL_3:def_2; then f in compactbelow x by A13, WAYBEL_8:4; hence v in pi ((compactbelow x),i) by A6, A11, CARD_3:def_6; ::_thesis: verum end; pi ((compactbelow x),i) c= compactbelow (x . i) proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in pi ((compactbelow x),i) or v in compactbelow (x . i) ) assume v in pi ((compactbelow x),i) ; ::_thesis: v in compactbelow (x . i) then consider f being Function such that A17: f in compactbelow x and A18: v = f . i by CARD_3:def_6; f in { y where y is Element of (product J) : ( x >= y & y is compact ) } by A17, WAYBEL_8:def_2; then consider f1 being Element of (product J) such that A19: f1 = f and A20: x >= f1 and A21: f1 is compact ; f1 << f1 by A21, WAYBEL_3:def_2; then f1 . i << f1 . i by A2, WAYBEL_3:33; then A22: f1 . i is compact by WAYBEL_3:def_2; f1 . i <= x . i by A20, WAYBEL_3:28; hence v in compactbelow (x . i) by A18, A19, A22, WAYBEL_8:4; ::_thesis: verum end; hence sup (compactbelow (x . i)) = sup (pi ((compactbelow x),i)) by A5, XBOOLE_0:def_10 .= (sup (compactbelow x)) . i by A2, WAYBEL_3:32 ; ::_thesis: verum end; now__::_thesis:_for_i_being_Element_of_I_holds_(sup_(compactbelow_x))_._i_<=_x_._i let i be Element of I; ::_thesis: (sup (compactbelow x)) . i <= x . i J . i is satisfying_axiom_K by A1; then x . i = sup (compactbelow (x . i)) by WAYBEL_8:def_3; hence (sup (compactbelow x)) . i <= x . i by A4; ::_thesis: verum end; then A23: sup (compactbelow x) <= x by WAYBEL_3:28; now__::_thesis:_for_i_being_Element_of_I_holds_x_._i_<=_(sup_(compactbelow_x))_._i let i be Element of I; ::_thesis: x . i <= (sup (compactbelow x)) . i J . i is satisfying_axiom_K by A1; then x . i = sup (compactbelow (x . i)) by WAYBEL_8:def_3; hence x . i <= (sup (compactbelow x)) . i by A4; ::_thesis: verum end; then x <= sup (compactbelow x) by WAYBEL_3:28; hence x = sup (compactbelow x) by A3, A23, YELLOW_0:def_3; ::_thesis: verum end; then A24: product J is satisfying_axiom_K by WAYBEL_8:def_3; A25: 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_c,_d_being_Element_of_L_st_c_in_compactbelow_x_&_d_in_compactbelow_x_holds_ ex_e_being_Element_of_the_carrier_of_L_st_ (_e_in_compactbelow_x_&_c_<=_e_&_d_<=_e_) let c, d be Element of L; ::_thesis: ( c in compactbelow x & d in compactbelow x implies ex e being Element of the carrier of L st ( e in compactbelow x & c <= e & d <= e ) ) assume that A26: c in compactbelow x and A27: d in compactbelow x ; ::_thesis: ex e being Element of the carrier of L st ( e in compactbelow x & c <= e & d <= e ) d is compact by A27, WAYBEL_8:4; then ( d <= c "\/" d & d << d ) by WAYBEL_3:def_2, YELLOW_0:22; then A28: d << c "\/" d by WAYBEL_3:2; c is compact by A26, WAYBEL_8:4; then ( c <= c "\/" d & c << c ) by WAYBEL_3:def_2, YELLOW_0:22; then c << c "\/" d by WAYBEL_3:2; then c "\/" d << c "\/" d by A28, WAYBEL_3:3; then A29: c "\/" d is compact by WAYBEL_3:def_2; take e = c "\/" d; ::_thesis: ( e in compactbelow x & c <= e & d <= e ) ( c <= x & d <= x ) by A26, A27, WAYBEL_8:4; then c "\/" d <= x by YELLOW_0:22; hence e in compactbelow x by A29, WAYBEL_8:4; ::_thesis: ( c <= e & d <= e ) thus ( c <= e & d <= e ) by YELLOW_0:22; ::_thesis: verum end; hence ( not compactbelow x is empty & compactbelow x is directed ) by WAYBEL_0:def_1; ::_thesis: verum end; L is up-complete by A2, WAYBEL_3:31; hence product J is lower-bounded algebraic LATTICE by A25, A24, WAYBEL_8:def_4; ::_thesis: verum end; Lm1: for L being lower-bounded LATTICE st L is algebraic holds ex X being non empty set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) proof let L be lower-bounded LATTICE; ::_thesis: ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ) assume A1: L is algebraic ; ::_thesis: ex X being non empty set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) then reconsider L9 = L as lower-bounded algebraic LATTICE ; take X = the carrier of (CompactSublatt L); ::_thesis: ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) consider g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) such that A2: g is infs-preserving and A3: g is directed-sups-preserving and A4: g is V13() and A5: for x being Element of L holds g . x = compactbelow x by A1, Th24; reconsider S = Image g as non empty full SubRelStr of BoolePoset X ; take S ; ::_thesis: ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) A6: L9 is complete ; hence S is infs-inheriting by A2, YELLOW_2:33; ::_thesis: ( S is directed-sups-inheriting & L,S are_isomorphic ) A7: rng g = the carrier of S by YELLOW_0:def_15; dom g = the carrier of L by FUNCT_2:def_1; then reconsider g1 = g as Function of L,S by A7, FUNCT_2:1; now__::_thesis:_for_x,_y_being_Element_of_L_holds_ (_(_x_<=_y_implies_g1_._x_<=_g1_._y_)_&_(_g1_._x_<=_g1_._y_implies_x_<=_y_)_) let x, y be Element of L; ::_thesis: ( ( x <= y implies g1 . x <= g1 . y ) & ( g1 . x <= g1 . y implies x <= y ) ) thus ( x <= y implies g1 . x <= g1 . y ) ::_thesis: ( g1 . x <= g1 . y implies x <= y ) proof assume x <= y ; ::_thesis: g1 . x <= g1 . y then compactbelow x c= compactbelow y by Th1; then g . x c= compactbelow y by A5; then g . x c= g . y by A5; then g . x <= g . y by YELLOW_1:2; hence g1 . x <= g1 . y by YELLOW_0:60; ::_thesis: verum end; thus ( g1 . x <= g1 . y implies x <= y ) ::_thesis: verum proof assume g1 . x <= g1 . y ; ::_thesis: x <= y then g . x <= g . y by YELLOW_0:59; then g . x c= g . y by YELLOW_1:2; then g . x c= compactbelow y by A5; then A8: compactbelow x c= compactbelow y by A5; ( ex_sup_of compactbelow x,L & ex_sup_of compactbelow y,L ) by A6, YELLOW_0:17; then sup (compactbelow x) <= sup (compactbelow y) by A8, YELLOW_0:34; then x <= sup (compactbelow y) by A1, WAYBEL_8:def_3; hence x <= y by A1, WAYBEL_8:def_3; ::_thesis: verum end; end; then A9: g1 is isomorphic by A4, A7, WAYBEL_0:66; then reconsider f1 = g1 " as Function of S,L by WAYBEL_0:67; A10: f1 is isomorphic by A9, WAYBEL_0:68; now__::_thesis:_for_Y_being_directed_Subset_of_S_st_Y_<>_{}_&_ex_sup_of_Y,_BoolePoset_X_holds_ "\/"_(Y,(BoolePoset_X))_in_the_carrier_of_S let Y be directed Subset of S; ::_thesis: ( Y <> {} & ex_sup_of Y, BoolePoset X implies "\/" (Y,(BoolePoset X)) in the carrier of S ) assume that A11: Y <> {} and ex_sup_of Y, BoolePoset X ; ::_thesis: "\/" (Y,(BoolePoset X)) in the carrier of S now__::_thesis:_for_X2_being_finite_Subset_of_(f1_.:_Y)_ex_f1y1_being_Element_of_the_carrier_of_L_st_ (_f1y1_in_f1_.:_Y_&_f1y1_is_>=_than_X2_) let X2 be finite Subset of (f1 .: Y); ::_thesis: ex f1y1 being Element of the carrier of L st ( f1y1 in f1 .: Y & f1y1 is_>=_than X2 ) A12: g1 " (g1 .: X2) c= X2 by A4, FUNCT_1:82; now__::_thesis:_for_v_being_set_st_v_in_g1_.:_X2_holds_ v_in_Y let v be set ; ::_thesis: ( v in g1 .: X2 implies v in Y ) assume v in g1 .: X2 ; ::_thesis: v in Y then ex u being set st ( u in dom g1 & u in X2 & v = g1 . u ) by FUNCT_1:def_6; then v in g1 .: (f1 .: Y) by FUNCT_1:def_6; then v in g1 .: (g1 " Y) by A4, FUNCT_1:85; hence v in Y by A7, FUNCT_1:77; ::_thesis: verum end; then reconsider Y1 = g1 .: X2 as finite Subset of Y by TARSKI:def_3; consider y1 being Element of S such that A13: y1 in Y and A14: y1 is_>=_than Y1 by A11, WAYBEL_0:1; take f1y1 = f1 . y1; ::_thesis: ( f1y1 in f1 .: Y & f1y1 is_>=_than X2 ) y1 in the carrier of S ; then y1 in dom f1 by FUNCT_2:def_1; hence f1y1 in f1 .: Y by A13, FUNCT_1:def_6; ::_thesis: f1y1 is_>=_than X2 X2 c= the carrier of L by XBOOLE_1:1; then X2 c= dom g1 by FUNCT_2:def_1; then A15: X2 c= g1 " (g1 .: X2) by FUNCT_1:76; f1 .: Y1 = g1 " (g1 .: X2) by A4, FUNCT_1:85 .= X2 by A15, A12, XBOOLE_0:def_10 ; hence f1y1 is_>=_than X2 by A10, A14, Th19; ::_thesis: verum end; then reconsider X1 = f1 .: Y as non empty directed Subset of L by WAYBEL_0:1; sup X1 in the carrier of L ; then sup X1 in dom g by FUNCT_2:def_1; then A16: g . (sup X1) in rng g by FUNCT_1:def_3; ( ex_sup_of X1,L & g preserves_sup_of X1 ) by A6, A3, WAYBEL_0:def_37, YELLOW_0:17; then A17: sup (g .: X1) in rng g by A16, WAYBEL_0:def_31; g .: X1 = g .: (g1 " Y) by A4, FUNCT_1:85 .= Y by A7, FUNCT_1:77 ; hence "\/" (Y,(BoolePoset X)) in the carrier of S by A17, YELLOW_0:def_15; ::_thesis: verum end; hence S is directed-sups-inheriting by WAYBEL_0:def_4; ::_thesis: L,S are_isomorphic thus L,S are_isomorphic by A9, WAYBEL_1:def_8; ::_thesis: verum end; theorem Th26: :: WAYBEL13:26 for L1, L2 being non empty RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds L1,L2 are_isomorphic proof let L1, L2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies L1,L2 are_isomorphic ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: L1,L2 are_isomorphic ex f being Function of L1,L2 st f is isomorphic proof reconsider f = id the carrier of L1 as Function of L1,L2 by A1; take f ; ::_thesis: f is isomorphic now__::_thesis:_for_z_being_set_st_z_in_the_carrier_of_L2_holds_ ex_v_being_set_st_ (_v_in_the_carrier_of_L1_&_z_=_f_._v_) let z be set ; ::_thesis: ( z in the carrier of L2 implies ex v being set st ( v in the carrier of L1 & z = f . v ) ) assume A2: z in the carrier of L2 ; ::_thesis: ex v being set st ( v in the carrier of L1 & z = f . v ) take v = z; ::_thesis: ( v in the carrier of L1 & z = f . v ) thus v in the carrier of L1 by A1, A2; ::_thesis: z = f . v thus z = f . v by A1, A2, FUNCT_1:18; ::_thesis: verum end; then A3: rng f = the carrier of L2 by FUNCT_2:10; for x, y being Element of L1 holds ( x <= y iff f . x <= f . y ) proof let x, y be Element of L1; ::_thesis: ( x <= y iff f . x <= f . y ) A4: ( f . x = x & f . y = y ) by FUNCT_1:18; hence ( x <= y implies f . x <= f . y ) by A1, YELLOW_0:1; ::_thesis: ( f . x <= f . y implies x <= y ) thus ( f . x <= f . y implies x <= y ) by A1, A4, YELLOW_0:1; ::_thesis: verum end; hence f is isomorphic by A3, WAYBEL_0:66; ::_thesis: verum end; hence L1,L2 are_isomorphic by WAYBEL_1:def_8; ::_thesis: verum end; Lm2: for L being LATTICE st ex X being non empty set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) proof let L be LATTICE; ::_thesis: ( ex X being non empty set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) ) given X being non empty set , S being full SubRelStr of BoolePoset X such that A1: S is infs-inheriting and A2: S is directed-sups-inheriting and A3: L,S are_isomorphic ; ::_thesis: ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) reconsider S9 = S as closure System of BoolePoset X by A1; take X ; ::_thesis: ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) reconsider c = closure_op S9 as closure Function of (BoolePoset X),(BoolePoset X) ; take c ; ::_thesis: ( c is directed-sups-preserving & L, Image c are_isomorphic ) thus c is directed-sups-preserving by A2; ::_thesis: L, Image c are_isomorphic Image c = RelStr(# the carrier of S, the InternalRel of S #) by WAYBEL10:18; then S, Image c are_isomorphic by Th26; hence L, Image c are_isomorphic by A3, WAYBEL_1:7; ::_thesis: verum end; Lm3: for L being LATTICE st ex X being set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) proof let L be LATTICE; ::_thesis: ( ex X being set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) ) given X being set , S being full SubRelStr of BoolePoset X such that A1: S is infs-inheriting and A2: S is directed-sups-inheriting and A3: L,S are_isomorphic ; ::_thesis: ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) reconsider S9 = S as closure System of BoolePoset X by A1; take X ; ::_thesis: ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) reconsider c = closure_op S9 as closure Function of (BoolePoset X),(BoolePoset X) ; take c ; ::_thesis: ( c is directed-sups-preserving & L, Image c are_isomorphic ) thus c is directed-sups-preserving by A2; ::_thesis: L, Image c are_isomorphic Image c = RelStr(# the carrier of S, the InternalRel of S #) by WAYBEL10:18; then S, Image c are_isomorphic by Th26; hence L, Image c are_isomorphic by A3, WAYBEL_1:7; ::_thesis: verum end; Lm4: for L1, L2 being non empty up-complete Poset for f being Function of L1,L2 st f is isomorphic holds for x, y being Element of L1 st x << y holds f . x << f . y proof let L1, L2 be non empty up-complete Poset; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds for x, y being Element of L1 st x << y holds f . x << f . y let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies for x, y being Element of L1 st x << y holds f . x << f . y ) assume A1: f is isomorphic ; ::_thesis: for x, y being Element of L1 st x << y holds f . x << f . y then reconsider g = f " as Function of L2,L1 by WAYBEL_0:67; let x, y be Element of L1; ::_thesis: ( x << y implies f . x << f . y ) A2: g is isomorphic by A1, WAYBEL_0:68; assume A3: x << y ; ::_thesis: f . x << f . y now__::_thesis:_for_X_being_non_empty_directed_Subset_of_L2_st_f_._y_<=_sup_X_holds_ ex_fc_being_Element_of_the_carrier_of_L2_st_ (_fc_in_X_&_f_._x_<=_fc_) let X be non empty directed Subset of L2; ::_thesis: ( f . y <= sup X implies ex fc being Element of the carrier of L2 st ( fc in X & f . x <= fc ) ) y in the carrier of L1 ; then A4: y in dom f by FUNCT_2:def_1; X c= the carrier of L2 ; then A5: X c= rng f by A1, WAYBEL_0:66; now__::_thesis:_for_Y1_being_finite_Subset_of_(g_.:_X)_ex_gy1_being_Element_of_the_carrier_of_L1_st_ (_gy1_in_g_.:_X_&_gy1_is_>=_than_Y1_) let Y1 be finite Subset of (g .: X); ::_thesis: ex gy1 being Element of the carrier of L1 st ( gy1 in g .: X & gy1 is_>=_than Y1 ) A6: f " (f .: Y1) c= Y1 by A1, FUNCT_1:82; now__::_thesis:_for_v_being_set_st_v_in_f_.:_Y1_holds_ v_in_X let v be set ; ::_thesis: ( v in f .: Y1 implies v in X ) assume v in f .: Y1 ; ::_thesis: v in X then ex u being set st ( u in dom f & u in Y1 & v = f . u ) by FUNCT_1:def_6; then v in f .: (g .: X) by FUNCT_1:def_6; then v in f .: (f " X) by A1, FUNCT_1:85; hence v in X by A5, FUNCT_1:77; ::_thesis: verum end; then reconsider X1 = f .: Y1 as finite Subset of X by TARSKI:def_3; consider y1 being Element of L2 such that A7: y1 in X and A8: y1 is_>=_than X1 by WAYBEL_0:1; take gy1 = g . y1; ::_thesis: ( gy1 in g .: X & gy1 is_>=_than Y1 ) y1 in the carrier of L2 ; then y1 in dom g by FUNCT_2:def_1; hence gy1 in g .: X by A7, FUNCT_1:def_6; ::_thesis: gy1 is_>=_than Y1 Y1 c= the carrier of L1 by XBOOLE_1:1; then Y1 c= dom f by FUNCT_2:def_1; then A9: Y1 c= f " (f .: Y1) by FUNCT_1:76; g .: X1 = f " (f .: Y1) by A1, FUNCT_1:85 .= Y1 by A9, A6, XBOOLE_0:def_10 ; hence gy1 is_>=_than Y1 by A2, A8, Th19; ::_thesis: verum end; then reconsider Y = g .: X as non empty directed Subset of L1 by WAYBEL_0:1; A10: ( ex_sup_of X,L2 & g preserves_sup_of X ) by A2, WAYBEL_0:75, WAYBEL_0:def_33; assume f . y <= sup X ; ::_thesis: ex fc being Element of the carrier of L2 st ( fc in X & f . x <= fc ) then g . (f . y) <= g . (sup X) by A2, WAYBEL_0:66; then y <= g . (sup X) by A1, A4, FUNCT_1:34; then y <= sup Y by A10, WAYBEL_0:def_31; then consider c being Element of L1 such that A11: c in Y and A12: x <= c by A3, WAYBEL_3:def_1; take fc = f . c; ::_thesis: ( fc in X & f . x <= fc ) c in the carrier of L1 ; then c in dom f by FUNCT_2:def_1; then f . c in f .: Y by A11, FUNCT_1:def_6; then f . c in f .: (f " X) by A1, FUNCT_1:85; hence fc in X by A5, FUNCT_1:77; ::_thesis: f . x <= fc thus f . x <= fc by A1, A12, WAYBEL_0:66; ::_thesis: verum end; hence f . x << f . y by WAYBEL_3:def_1; ::_thesis: verum end; theorem Th27: :: WAYBEL13:27 for L1, L2 being non empty up-complete Poset for f being Function of L1,L2 st f is isomorphic holds for x, y being Element of L1 holds ( x << y iff f . x << f . y ) proof let L1, L2 be non empty up-complete Poset; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds for x, y being Element of L1 holds ( x << y iff f . x << f . y ) let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies for x, y being Element of L1 holds ( x << y iff f . x << f . y ) ) assume A1: f is isomorphic ; ::_thesis: for x, y being Element of L1 holds ( x << y iff f . x << f . y ) then reconsider g = f " as Function of L2,L1 by WAYBEL_0:67; let x, y be Element of L1; ::_thesis: ( x << y iff f . x << f . y ) thus ( x << y implies f . x << f . y ) by A1, Lm4; ::_thesis: ( f . x << f . y implies x << y ) thus ( f . x << f . y implies x << y ) ::_thesis: verum proof y in the carrier of L1 ; then A2: y in dom f by FUNCT_2:def_1; x in the carrier of L1 ; then A3: x in dom f by FUNCT_2:def_1; assume f . x << f . y ; ::_thesis: x << y then g . (f . x) << g . (f . y) by A1, Lm4, WAYBEL_0:68; then x << g . (f . y) by A1, A3, FUNCT_1:34; hence x << y by A1, A2, FUNCT_1:34; ::_thesis: verum end; end; theorem Th28: :: WAYBEL13:28 for L1, L2 being non empty up-complete Poset for f being Function of L1,L2 st f is isomorphic holds for x being Element of L1 holds ( x is compact iff f . x is compact ) proof let L1, L2 be non empty up-complete Poset; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds for x being Element of L1 holds ( x is compact iff f . x is compact ) let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies for x being Element of L1 holds ( x is compact iff f . x is compact ) ) assume A1: f is isomorphic ; ::_thesis: for x being Element of L1 holds ( x is compact iff f . x is compact ) let x be Element of L1; ::_thesis: ( x is compact iff f . x is compact ) thus ( x is compact implies f . x is compact ) ::_thesis: ( f . x is compact implies x is compact ) proof assume x is compact ; ::_thesis: f . x is compact then x << x by WAYBEL_3:def_2; then f . x << f . x by A1, Th27; hence f . x is compact by WAYBEL_3:def_2; ::_thesis: verum end; thus ( f . x is compact implies x is compact ) ::_thesis: verum proof assume f . x is compact ; ::_thesis: x is compact then f . x << f . x by WAYBEL_3:def_2; then x << x by A1, Th27; hence x is compact by WAYBEL_3:def_2; ::_thesis: verum end; end; theorem Th29: :: WAYBEL13:29 for L1, L2 being non empty up-complete Poset for f being Function of L1,L2 st f is isomorphic holds for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x) proof let L1, L2 be non empty up-complete Poset; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x) let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x) ) assume A1: f is isomorphic ; ::_thesis: for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x) then reconsider g = f " as Function of L2,L1 by WAYBEL_0:67; let x be Element of L1; ::_thesis: f .: (compactbelow x) = compactbelow (f . x) A2: g is isomorphic by A1, WAYBEL_0:68; A3: compactbelow (f . x) c= f .: (compactbelow x) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in compactbelow (f . x) or z in f .: (compactbelow x) ) x in the carrier of L1 ; then A4: x in dom f by FUNCT_2:def_1; assume z in compactbelow (f . x) ; ::_thesis: z in f .: (compactbelow x) then z in { y where y is Element of L2 : ( f . x >= y & y is compact ) } by WAYBEL_8:def_2; then consider z1 being Element of L2 such that A5: z1 = z and A6: f . x >= z1 and A7: z1 is compact ; A8: g . z1 is compact by A2, A7, Th28; g . z1 <= g . (f . x) by A2, A6, WAYBEL_0:66; then g . z1 <= x by A1, A4, FUNCT_1:34; then A9: g . z1 in compactbelow x by A8, WAYBEL_8:4; z1 in the carrier of L2 ; then A10: z1 in rng f by A1, WAYBEL_0:66; g . z1 in the carrier of L1 ; then g . z1 in dom f by FUNCT_2:def_1; then f . (g . z1) in f .: (compactbelow x) by A9, FUNCT_1:def_6; hence z in f .: (compactbelow x) by A1, A5, A10, FUNCT_1:35; ::_thesis: verum end; f .: (compactbelow x) c= compactbelow (f . x) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in f .: (compactbelow x) or z in compactbelow (f . x) ) assume z in f .: (compactbelow x) ; ::_thesis: z in compactbelow (f . x) then consider u being set such that u in dom f and A11: u in compactbelow x and A12: z = f . u by FUNCT_1:def_6; u in { y where y is Element of L1 : ( x >= y & y is compact ) } by A11, WAYBEL_8:def_2; then consider u1 being Element of L1 such that A13: u1 = u and A14: ( x >= u1 & u1 is compact ) ; ( f . u1 <= f . x & f . u1 is compact ) by A1, A14, Th28, WAYBEL_0:66; hence z in compactbelow (f . x) by A12, A13, WAYBEL_8:4; ::_thesis: verum end; hence f .: (compactbelow x) = compactbelow (f . x) by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th30: :: WAYBEL13:30 for L1, L2 being non empty Poset st L1,L2 are_isomorphic & L1 is up-complete holds L2 is up-complete proof let L1, L2 be non empty Poset; ::_thesis: ( L1,L2 are_isomorphic & L1 is up-complete implies L2 is up-complete ) assume that A1: L1,L2 are_isomorphic and A2: L1 is up-complete ; ::_thesis: L2 is up-complete consider f being Function of L1,L2 such that A3: f is isomorphic by A1, WAYBEL_1:def_8; reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67; A4: g is isomorphic by A3, WAYBEL_0:68; now__::_thesis:_for_Y_being_non_empty_directed_Subset_of_L2_holds_ex_sup_of_Y,L2 let Y be non empty directed Subset of L2; ::_thesis: ex_sup_of Y,L2 Y c= the carrier of L2 ; then A5: Y c= rng f by A3, WAYBEL_0:66; now__::_thesis:_for_X1_being_finite_Subset_of_(g_.:_Y)_ex_gy1_being_Element_of_the_carrier_of_L1_st_ (_gy1_in_g_.:_Y_&_gy1_is_>=_than_X1_) let X1 be finite Subset of (g .: Y); ::_thesis: ex gy1 being Element of the carrier of L1 st ( gy1 in g .: Y & gy1 is_>=_than X1 ) A6: f " (f .: X1) c= X1 by A3, FUNCT_1:82; now__::_thesis:_for_v_being_set_st_v_in_f_.:_X1_holds_ v_in_Y let v be set ; ::_thesis: ( v in f .: X1 implies v in Y ) assume v in f .: X1 ; ::_thesis: v in Y then ex u being set st ( u in dom f & u in X1 & v = f . u ) by FUNCT_1:def_6; then v in f .: (g .: Y) by FUNCT_1:def_6; then v in f .: (f " Y) by A3, FUNCT_1:85; hence v in Y by A5, FUNCT_1:77; ::_thesis: verum end; then reconsider Y1 = f .: X1 as finite Subset of Y by TARSKI:def_3; consider y1 being Element of L2 such that A7: y1 in Y and A8: y1 is_>=_than Y1 by WAYBEL_0:1; take gy1 = g . y1; ::_thesis: ( gy1 in g .: Y & gy1 is_>=_than X1 ) y1 in the carrier of L2 ; then y1 in dom g by FUNCT_2:def_1; hence gy1 in g .: Y by A7, FUNCT_1:def_6; ::_thesis: gy1 is_>=_than X1 X1 c= the carrier of L1 by XBOOLE_1:1; then X1 c= dom f by FUNCT_2:def_1; then A9: X1 c= f " (f .: X1) by FUNCT_1:76; g .: Y1 = f " (f .: X1) by A3, FUNCT_1:85 .= X1 by A9, A6, XBOOLE_0:def_10 ; hence gy1 is_>=_than X1 by A4, A8, Th19; ::_thesis: verum end; then reconsider X = g .: Y as non empty directed Subset of L1 by WAYBEL_0:1; ex_sup_of X,L1 by A2, WAYBEL_0:75; then consider x being Element of L1 such that A10: X is_<=_than x and A11: for b being Element of L1 st X is_<=_than b holds x <= b by YELLOW_0:15; A12: now__::_thesis:_for_y_being_Element_of_L2_st_Y_is_<=_than_y_holds_ f_._x_<=_y let y be Element of L2; ::_thesis: ( Y is_<=_than y implies f . x <= y ) assume Y is_<=_than y ; ::_thesis: f . x <= y then X is_<=_than g . y by A4, Th19; then x <= g . y by A11; then A13: f . x <= f . (g . y) by A3, WAYBEL_0:66; y in the carrier of L2 ; then y in dom g by FUNCT_2:def_1; then y in rng f by A3, FUNCT_1:33; hence f . x <= y by A3, A13, FUNCT_1:35; ::_thesis: verum end; f .: X = f .: (f " Y) by A3, FUNCT_1:85 .= Y by A5, FUNCT_1:77 ; then Y is_<=_than f . x by A3, A10, Th19; hence ex_sup_of Y,L2 by A12, YELLOW_0:15; ::_thesis: verum end; hence L2 is up-complete by WAYBEL_0:75; ::_thesis: verum end; theorem Th31: :: WAYBEL13:31 for L1, L2 being non empty Poset st L1,L2 are_isomorphic & L1 is complete & L1 is satisfying_axiom_K holds L2 is satisfying_axiom_K proof let L1, L2 be non empty Poset; ::_thesis: ( L1,L2 are_isomorphic & L1 is complete & L1 is satisfying_axiom_K implies L2 is satisfying_axiom_K ) assume that A1: L1,L2 are_isomorphic and A2: ( L1 is complete & L1 is satisfying_axiom_K ) ; ::_thesis: L2 is satisfying_axiom_K consider f being Function of L1,L2 such that A3: f is isomorphic by A1, WAYBEL_1:def_8; reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67; now__::_thesis:_for_x_being_Element_of_L2_holds_x_=_sup_(compactbelow_x) let x be Element of L2; ::_thesis: x = sup (compactbelow x) A4: ( f preserves_sup_of compactbelow (g . x) & ex_sup_of compactbelow (g . x),L1 ) by A2, A3, WAYBEL_0:def_33, YELLOW_0:17; A5: L2 is non empty up-complete Poset by A1, A2, Th30; x in the carrier of L2 ; then x in dom g by FUNCT_2:def_1; then A6: x in rng f by A3, FUNCT_1:33; hence x = f . (g . x) by A3, FUNCT_1:35 .= f . (sup (compactbelow (g . x))) by A2, WAYBEL_8:def_3 .= sup (f .: (compactbelow (g . x))) by A4, WAYBEL_0:def_31 .= sup (compactbelow (f . (g . x))) by A2, A3, A5, Th29 .= sup (compactbelow x) by A3, A6, FUNCT_1:35 ; ::_thesis: verum end; hence L2 is satisfying_axiom_K by WAYBEL_8:def_3; ::_thesis: verum end; theorem Th32: :: WAYBEL13:32 for L1, L2 being sup-Semilattice st L1,L2 are_isomorphic & L1 is lower-bounded & L1 is algebraic holds L2 is algebraic proof let L1, L2 be sup-Semilattice; ::_thesis: ( L1,L2 are_isomorphic & L1 is lower-bounded & L1 is algebraic implies L2 is algebraic ) assume that A1: L1,L2 are_isomorphic and A2: ( L1 is lower-bounded & L1 is algebraic ) ; ::_thesis: L2 is algebraic consider f being Function of L1,L2 such that A3: f is isomorphic by A1, WAYBEL_1:def_8; reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67; A4: g is isomorphic by A3, WAYBEL_0:68; A5: now__::_thesis:_for_y_being_Element_of_L2_holds_ (_not_compactbelow_y_is_empty_&_compactbelow_y_is_directed_) let y be Element of L2; ::_thesis: ( not compactbelow y is empty & compactbelow y is directed ) y in the carrier of L2 ; then y in dom g by FUNCT_2:def_1; then A6: y in rng f by A3, FUNCT_1:33; A7: L2 is non empty up-complete Poset by A1, A2, Th30; A8: ( not compactbelow (g . y) is empty & compactbelow (g . y) is directed ) by A2, WAYBEL_8:def_4; now__::_thesis:_for_Y_being_finite_Subset_of_(compactbelow_(f_._(g_._y)))_ex_fx_being_Element_of_the_carrier_of_L2_st_ (_fx_in_compactbelow_(f_._(g_._y))_&_fx_is_>=_than_Y_) let Y be finite Subset of (compactbelow (f . (g . y))); ::_thesis: ex fx being Element of the carrier of L2 st ( fx in compactbelow (f . (g . y)) & fx is_>=_than Y ) Y c= the carrier of L2 by XBOOLE_1:1; then A9: Y c= rng f by A3, WAYBEL_0:66; now__::_thesis:_for_z_being_set_st_z_in_g_.:_Y_holds_ z_in_compactbelow_(g_._y) let z be set ; ::_thesis: ( z in g .: Y implies z in compactbelow (g . y) ) assume z in g .: Y ; ::_thesis: z in compactbelow (g . y) then consider v being set such that A10: v in dom g and A11: v in Y and A12: z = g . v by FUNCT_1:def_6; reconsider v = v as Element of L2 by A10; v in compactbelow (f . (g . y)) by A11; then v in compactbelow y by A3, A6, FUNCT_1:35; then v <= y by WAYBEL_8:4; then A13: g . v <= g . y by A4, WAYBEL_0:66; v is compact by A11, WAYBEL_8:4; then g . v is compact by A2, A4, A7, Th28; hence z in compactbelow (g . y) by A12, A13, WAYBEL_8:4; ::_thesis: verum end; then reconsider X = g .: Y as finite Subset of (compactbelow (g . y)) by TARSKI:def_3; consider x being Element of L1 such that A14: x in compactbelow (g . y) and A15: x is_>=_than X by A8, WAYBEL_0:1; take fx = f . x; ::_thesis: ( fx in compactbelow (f . (g . y)) & fx is_>=_than Y ) x <= g . y by A14, WAYBEL_8:4; then A16: f . x <= f . (g . y) by A3, WAYBEL_0:66; x is compact by A14, WAYBEL_8:4; then f . x is compact by A2, A3, A7, Th28; hence fx in compactbelow (f . (g . y)) by A16, WAYBEL_8:4; ::_thesis: fx is_>=_than Y f .: X = f .: (f " Y) by A3, FUNCT_1:85 .= Y by A9, FUNCT_1:77 ; hence fx is_>=_than Y by A3, A15, Th19; ::_thesis: verum end; then ( not compactbelow (f . (g . y)) is empty & compactbelow (f . (g . y)) is directed ) by WAYBEL_0:1; hence ( not compactbelow y is empty & compactbelow y is directed ) by A3, A6, FUNCT_1:35; ::_thesis: verum end; ( L2 is up-complete & L2 is satisfying_axiom_K ) by A1, A2, Th30, Th31; hence L2 is algebraic by A5, WAYBEL_8:def_4; ::_thesis: verum end; Lm5: for L being LATTICE st ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) holds L is algebraic proof let L be LATTICE; ::_thesis: ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) given X being set , c being closure Function of (BoolePoset X),(BoolePoset X) such that A1: c is directed-sups-preserving and A2: L, Image c are_isomorphic ; ::_thesis: L is algebraic ( Image c is complete LATTICE & Image c is algebraic LATTICE ) by A1, WAYBEL_8:24, YELLOW_2:35; hence L is algebraic by A2, Th32, WAYBEL_1:6; ::_thesis: verum end; theorem :: WAYBEL13:33 for L being lower-bounded continuous sup-Semilattice holds ( SupMap L is infs-preserving & SupMap L is sups-preserving ) by WAYBEL_1:12, WAYBEL_1:57, WAYBEL_5:3; theorem :: WAYBEL13:34 for L being lower-bounded LATTICE holds ( ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ) & ( ex X being set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ) ) proof let L be lower-bounded LATTICE; ::_thesis: ( ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ) & ( ex X being set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ) ) thus ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ) by Lm1; ::_thesis: ( ex X being set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ) thus ( ex X being set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ) ::_thesis: verum proof assume ex X being set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ; ::_thesis: L is algebraic then ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) by Lm3; hence L is algebraic by Lm5; ::_thesis: verum end; end; theorem :: WAYBEL13:35 for L being lower-bounded LATTICE holds ( ( L is algebraic implies ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) ) & ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) ) proof let L be lower-bounded LATTICE; ::_thesis: ( ( L is algebraic implies ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) ) & ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) ) hereby ::_thesis: ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) assume L is algebraic ; ::_thesis: ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) then ex X being non empty set ex S being full SubRelStr of BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) by Lm1; hence ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) by Lm2; ::_thesis: verum end; thus ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st ( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) by Lm5; ::_thesis: verum end;