:: WAYBEL_8 semantic presentation

begin

definition
let L be non empty reflexive RelStr ;
func CompactSublatt L ->  strict full SubRelStr of L means :Def1: :: WAYBEL_8:def 1
 for x being Element of L holds
( x in the carrier of it iff x is compact );
existence
 ex b1 being strict full SubRelStr of L st
for x being Element of L holds
( x in the carrier of b1 iff x is compact )
proof
defpred S1[ set ] means  ex y being Element of L st
( y = $1 & y is compact );
consider X being Subset of L such that
A1: for x being set holds
( x in X iff ( x in the carrier of L & S1[x] ) ) from SUBSET_1:sch_1();
reconsider S = RelStr(# X,( the InternalRel of L |_2 X) #) as strict full SubRelStr of L by YELLOW_0:56;
take  S ; ::_thesis: for x being Element of L holds
( x in the carrier of S iff x is compact )
let x be Element of L; ::_thesis: ( x in the carrier of S iff x is compact )
thus  ( x in the carrier of S implies x is compact ) ::_thesis: ( x is compact implies x in the carrier of S )
proof
assume  x in the carrier of S ; ::_thesis: x is compact
then  ex y being Element of L st
( y = x & y is compact ) by A1;
hence  x is compact ; ::_thesis: verum
end;
thus  ( x is compact implies x in the carrier of S ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict full SubRelStr of L st ( for x being Element of L holds
( x in the carrier of b1 iff x is compact ) ) & ( for x being Element of L holds
( x in the carrier of b2 iff x is compact ) ) holds
b1 = b2
proof
let K1, K2 be strict full SubRelStr of L; ::_thesis: ( ( for x being Element of L holds
( x in the carrier of K1 iff x is compact ) ) & ( for x being Element of L holds
( x in the carrier of K2 iff x is compact ) ) implies K1 = K2 )
assume that
A2: for x being Element of L holds
( x in the carrier of K1 iff x is compact ) and
A3: for x being Element of L holds
( x in the carrier of K2 iff x is compact ) ; ::_thesis: K1 = K2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_the_carrier_of_K1_implies_x_in_the_carrier_of_K2_)_&_(_x_in_the_carrier_of_K2_implies_x_in_the_carrier_of_K1_)_)
let x be set ; ::_thesis: ( ( x in the carrier of K1 implies x in the carrier of K2 ) & ( x in the carrier of K2 implies x in the carrier of K1 ) )
thus  ( x in the carrier of K1 implies x in the carrier of K2 ) ::_thesis: ( x in the carrier of K2 implies x in the carrier of K1 )
proof
assume A4: x in the carrier of K1 ; ::_thesis: x in the carrier of K2
 the carrier of K1 c= the carrier of L by YELLOW_0:def_13;
then reconsider x9 = x as Element of L by A4;
 x9 is compact by A2, A4;
hence  x in the carrier of K2 by A3; ::_thesis: verum
end;
thus  ( x in the carrier of K2 implies x in the carrier of K1 ) ::_thesis: verum
proof
assume A5: x in the carrier of K2 ; ::_thesis: x in the carrier of K1
 the carrier of K2 c= the carrier of L by YELLOW_0:def_13;
then reconsider x9 = x as Element of L by A5;
 x9 is compact by A3, A5;
hence  x in the carrier of K1 by A2; ::_thesis: verum
end;
end;
then  the carrier of K1 = the carrier of K2 by TARSKI:1;
hence  K1 = K2 by YELLOW_0:57; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines CompactSublatt WAYBEL_8:def_1_:_
 for L being non empty reflexive RelStr
for b2 being strict full SubRelStr of L holds
( b2 = CompactSublatt L iff for x being Element of L holds
( x in the carrier of b2 iff x is compact ) );

registration
let L be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster CompactSublatt L ->  non empty strict full ;
coherence
 not CompactSublatt L is empty
proof
 Bottom L is compact by WAYBEL_3:15;
hence  not CompactSublatt L is empty by Def1; ::_thesis: verum
end;
end;

theorem :: WAYBEL_8:1
for L being complete LATTICE
for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds
x << y
proof
let L be complete LATTICE; ::_thesis: for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds
x << y
let x, y, k be Element of L; ::_thesis: ( x <= k & k <= y & k in the carrier of (CompactSublatt L) implies x << y )
assume that
A1: ( x <= k & k <= y ) and
A2: k in the carrier of (CompactSublatt L) ; ::_thesis: x << y
 k is compact by A2, Def1;
then  k << k by WAYBEL_3:def_2;
hence  x << y by A1, WAYBEL_3:2; ::_thesis: verum
end;

theorem :: WAYBEL_8:2
for L being complete LATTICE
for x being Element of L holds
( uparrow x is Open Filter of L iff x is compact )
proof
let L be complete LATTICE; ::_thesis: for x being Element of L holds
( uparrow x is Open Filter of L iff x is compact )
let x be Element of L; ::_thesis: ( uparrow x is Open Filter of L iff x is compact )
thus  ( uparrow x is Open Filter of L implies x is compact ) ::_thesis: ( x is compact implies uparrow x is Open Filter of L )
proof
 x <= x ;
then A1: x in uparrow x by WAYBEL_0:18;
assume  uparrow x is Open Filter of L ; ::_thesis: x is compact
then consider y being Element of L such that
A2: y in uparrow x and
A3: y << x by A1, WAYBEL_6:def_1;
 x <= y by A2, WAYBEL_0:18;
then  x << x by A3, WAYBEL_3:2;
hence  x is compact by WAYBEL_3:def_2; ::_thesis: verum
end;
assume A4: x is compact ; ::_thesis: uparrow x is Open Filter of L
now__::_thesis:_for_u_being_Element_of_L_st_u_in_uparrow_x_holds_
ex_x2_being_Element_of_L_st_
(_x2_in_uparrow_x_&_x2_<<_u_)
let u be Element of L; ::_thesis: ( u in uparrow x implies ex x2 being Element of L st
( x2 in uparrow x & x2 << u ) )
assume  u in uparrow x ; ::_thesis: ex x2 being Element of L st
( x2 in uparrow x & x2 << u )
then A5: x <= u by WAYBEL_0:18;
take x2 = x; ::_thesis: ( x2 in uparrow x & x2 << u )
 x <= x2 ;
hence  x2 in uparrow x by WAYBEL_0:18; ::_thesis: x2 << u
 x << x by A4, WAYBEL_3:def_2;
hence  x2 << u by A5, WAYBEL_3:2; ::_thesis: verum
end;
hence  uparrow x is Open Filter of L by WAYBEL_6:def_1; ::_thesis: verum
end;

theorem :: WAYBEL_8:3
for L being non empty with_suprema lower-bounded Poset holds
( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) )
proof
let L be non empty with_suprema lower-bounded Poset; ::_thesis: ( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) )
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(CompactSublatt_L)_&_y_in_the_carrier_of_(CompactSublatt_L)_&_ex_sup_of_{x,y},L_holds_
sup_{x,y}_in_the_carrier_of_(CompactSublatt_L)
let x, y be Element of L; ::_thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_sup_of {x,y},L implies sup {x,y} in the carrier of (CompactSublatt L) )
assume that
A1: x in the carrier of (CompactSublatt L) and
A2: y in the carrier of (CompactSublatt L) and
A3: ex_sup_of {x,y},L ; ::_thesis: sup {x,y} in the carrier of (CompactSublatt L)
 y is compact by A2, Def1;
then A4: y << y by WAYBEL_3:def_2;
 x is compact by A1, Def1;
then A5: x << x by WAYBEL_3:def_2;
 y <= x "\/" y by A3, YELLOW_0:18;
then A6: y << x "\/" y by A4, WAYBEL_3:2;
 x <= x "\/" y by A3, YELLOW_0:18;
then  x << x "\/" y by A5, WAYBEL_3:2;
then  x "\/" y << x "\/" y by A6, WAYBEL_3:3;
then  x "\/" y is compact by WAYBEL_3:def_2;
then  sup {x,y} is compact by YELLOW_0:41;
hence  sup {x,y} in the carrier of (CompactSublatt L) by Def1; ::_thesis: verum
end;
hence  CompactSublatt L is join-inheriting by YELLOW_0:def_17; ::_thesis: Bottom L in the carrier of (CompactSublatt L)
 Bottom L is compact by WAYBEL_3:15;
hence  Bottom L in the carrier of (CompactSublatt L) by Def1; ::_thesis: verum
end;

definition
let L be non empty reflexive RelStr ;
let x be Element of L;
func compactbelow x ->  Subset of L equals :: WAYBEL_8:def 2
 {  y where y is Element of L : ( x >= y & y is compact )  }  ;
coherence
  {  y where y is Element of L : ( x >= y & y is compact )  }  is Subset of L
proof
set Z =  {  y where y is Element of L : ( x >= y & y is compact )  }  ;
defpred S1[ Element of L] means ( x >= $1 & $1 is compact );
consider X being Subset of L such that
A1: for y being Element of L holds
( y in X iff S1[y] ) from SUBSET_1:sch_3();
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_X_implies_z_in__{__y_where_y_is_Element_of_L_:_(_x_>=_y_&_y_is_compact_)__}__)_&_(_z_in__{__y_where_y_is_Element_of_L_:_(_x_>=_y_&_y_is_compact_)__}__implies_z_in_X_)_)
let z be set ; ::_thesis: ( ( z in X implies z in  {  y where y is Element of L : ( x >= y & y is compact )  }  ) & ( z in  {  y where y is Element of L : ( x >= y & y is compact )  }  implies z in X ) )
thus  ( z in X implies z in  {  y where y is Element of L : ( x >= y & y is compact )  }  ) ::_thesis: ( z in  {  y where y is Element of L : ( x >= y & y is compact )  }  implies z in X )
proof
assume A2: z in X ; ::_thesis: z in  {  y where y is Element of L : ( x >= y & y is compact )  }
then reconsider z1 = z as Element of L ;
 ( x >= z1 & z1 is compact ) by A1, A2;
hence  z in  {  y where y is Element of L : ( x >= y & y is compact )  }  ; ::_thesis: verum
end;
thus  ( z in  {  y where y is Element of L : ( x >= y & y is compact )  }  implies z in X ) ::_thesis: verum
proof
assume  z in  {  y where y is Element of L : ( x >= y & y is compact )  }  ; ::_thesis: z in X
then  ex v being Element of L st
( v = z & x >= v & v is compact ) ;
hence  z in X by A1; ::_thesis: verum
end;
end;
hence   {  y where y is Element of L : ( x >= y & y is compact )  }  is Subset of L by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem  defines compactbelow WAYBEL_8:def_2_:_
 for L being non empty reflexive RelStr
for x being Element of L holds compactbelow x =  {  y where y is Element of L : ( x >= y & y is compact )  }  ;

theorem Th4: :: WAYBEL_8:4
for L being non empty reflexive RelStr
for x, y being Element of L holds
( y in compactbelow x iff ( x >= y & y is compact ) )
proof
let L be non empty reflexive RelStr ; ::_thesis: for x, y being Element of L holds
( y in compactbelow x iff ( x >= y & y is compact ) )
let x, y be Element of L; ::_thesis: ( y in compactbelow x iff ( x >= y & y is compact ) )
thus  ( y in compactbelow x implies ( x >= y & y is compact ) ) ::_thesis: ( x >= y & y is compact implies y in compactbelow x )
proof
assume  y in compactbelow x ; ::_thesis: ( x >= y & y is compact )
then  ex z being Element of L st
( z = y & x >= z & z is compact ) ;
hence  ( x >= y & y is compact ) ; ::_thesis: verum
end;
assume  ( x >= y & y is compact ) ; ::_thesis: y in compactbelow x
hence  y in compactbelow x ; ::_thesis: verum
end;

theorem Th5: :: WAYBEL_8:5
for L being non empty reflexive RelStr
for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)
proof
let L be non empty reflexive RelStr ; ::_thesis: for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)
let x be Element of L; ::_thesis: compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)
now__::_thesis:_for_y_being_set_st_y_in_(downarrow_x)_/\_the_carrier_of_(CompactSublatt_L)_holds_
y_in_compactbelow_x
let y be set ; ::_thesis: ( y in (downarrow x) /\ the carrier of (CompactSublatt L) implies y in compactbelow x )
assume A1: y in (downarrow x) /\ the carrier of (CompactSublatt L) ; ::_thesis: y in compactbelow x
then reconsider y9 = y as Element of L ;
 y in downarrow x by A1, XBOOLE_0:def_4;
then A2: y9 <= x by WAYBEL_0:17;
 y in the carrier of (CompactSublatt L) by A1, XBOOLE_0:def_4;
then  y9 is compact by Def1;
hence  y in compactbelow x by A2; ::_thesis: verum
end;
then A3: (downarrow x) /\ the carrier of (CompactSublatt L) c= compactbelow x by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_compactbelow_x_holds_
y_in_(downarrow_x)_/\_the_carrier_of_(CompactSublatt_L)
let y be set ; ::_thesis: ( y in compactbelow x implies y in (downarrow x) /\ the carrier of (CompactSublatt L) )
assume  y in compactbelow x ; ::_thesis: y in (downarrow x) /\ the carrier of (CompactSublatt L)
then consider y9 being Element of L such that
A4: y9 = y and
A5: ( y9 <= x & y9 is compact ) ;
 ( y9 in downarrow x & y9 in the carrier of (CompactSublatt L) ) by A5, Def1, WAYBEL_0:17;
hence  y in (downarrow x) /\ the carrier of (CompactSublatt L) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
then  compactbelow x c= (downarrow x) /\ the carrier of (CompactSublatt L) by TARSKI:def_3;
hence  compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th6: :: WAYBEL_8:6
for L being non empty reflexive transitive RelStr
for x being Element of L holds compactbelow x c= waybelow x
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for x being Element of L holds compactbelow x c= waybelow x
let x be Element of L; ::_thesis: compactbelow x c= waybelow x
now__::_thesis:_for_z_being_set_st_z_in_compactbelow_x_holds_
z_in_waybelow_x
let z be set ; ::_thesis: ( z in compactbelow x implies z in waybelow x )
assume  z in compactbelow x ; ::_thesis: z in waybelow x
then consider z9 being Element of L such that
A1: z9 = z and
A2: x >= z9 and
A3: z9 is compact ;
 z9 << z9 by A3, WAYBEL_3:def_2;
then  z9 << x by A2, WAYBEL_3:2;
hence  z in waybelow x by A1, WAYBEL_3:7; ::_thesis: verum
end;
hence  compactbelow x c= waybelow x by TARSKI:def_3; ::_thesis: verum
end;

registration
let L be non empty reflexive antisymmetric lower-bounded RelStr ;
let x be Element of L;
cluster compactbelow x ->  non empty ;
coherence
 not compactbelow x is empty
proof
 ( x >= Bottom L & Bottom L is compact ) by WAYBEL_3:15, YELLOW_0:44;
then  Bottom L in  {  y where y is Element of L : ( x >= y & y is compact )  }  ;
hence  not compactbelow x is empty ; ::_thesis: verum
end;
end;

begin

definition
let L be non empty reflexive RelStr ;
attrL is satisfying_axiom_K  means :Def3: :: WAYBEL_8:def 3
 for x being Element of L holds x = sup (compactbelow x);
end;

:: deftheorem Def3 defines satisfying_axiom_K WAYBEL_8:def_3_:_
 for L being non empty reflexive RelStr holds
( L is satisfying_axiom_K iff for x being Element of L holds x = sup (compactbelow x) );

definition
let L be non empty reflexive RelStr ;
attrL is algebraic  means :Def4: :: WAYBEL_8:def 4
( ( for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K );
end;

:: deftheorem Def4 defines algebraic WAYBEL_8:def_4_:_
 for L being non empty reflexive RelStr holds
( L is algebraic iff ( ( for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K ) );

theorem Th7: :: WAYBEL_8:7
for L being LATTICE holds
( L is algebraic iff ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) )
proof
let L be LATTICE; ::_thesis: ( L is algebraic iff ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) )
thus  ( L is algebraic implies ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) ) ::_thesis: ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) implies L is algebraic )
proof
assume A1: L is algebraic ; ::_thesis: ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) )
then A2: ( L is up-complete & L is satisfying_axiom_K ) by Def4;
now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_(waybelow_x)
let x be Element of L; ::_thesis: x = sup (waybelow x)
A3: ( not compactbelow x is empty & compactbelow x is directed ) by A1, Def4;
then A4: ex s being set st s in compactbelow x by XBOOLE_0:def_1;
 compactbelow x c= waybelow x by Th6;
then A5: ex_sup_of waybelow x,L by A2, A4, WAYBEL_0:75;
 ex_sup_of compactbelow x,L by A2, A3, WAYBEL_0:75;
then  sup (compactbelow x) <= sup (waybelow x) by A5, Th6, YELLOW_0:34;
then A6: x <= sup (waybelow x) by A2, Def3;
 waybelow x is_<=_than x by WAYBEL_3:9;
then  sup (waybelow x) <= x by A5, YELLOW_0:def_9;
hence  x = sup (waybelow x) by A6, ORDERS_2:2; ::_thesis: verum
end;
then A7: L is satisfying_axiom_of_approximation by WAYBEL_3:def_5;
 for x being Element of L holds
( not waybelow x is empty & waybelow x is directed )
proof
let x be Element of L; ::_thesis: ( not waybelow x is empty & waybelow x is directed )
 compactbelow x c= waybelow x by Th6;
hence  ( not waybelow x is empty & waybelow x is directed ) by A1, Def4; ::_thesis: verum
end;
hence  L is continuous by A2, A7, WAYBEL_3:def_6; ::_thesis: for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y )
let x, y be Element of L; ::_thesis: ( x << y implies ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) )
reconsider D = compactbelow y as non empty directed Subset of L by A1, Def4;
assume A8: x << y ; ::_thesis: ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y )
 y = sup D by A2, Def3;
then consider d being Element of L such that
A9: d in D and
A10: x <= d by A8, WAYBEL_3:def_1;
take  d ; ::_thesis: ( d in the carrier of (CompactSublatt L) & x <= d & d <= y )
 d is compact by A9, Th4;
hence  d in the carrier of (CompactSublatt L) by Def1; ::_thesis: ( x <= d & d <= y )
thus  ( x <= d & d <= y ) by A9, A10, Th4; ::_thesis: verum
end;
assume that
A11: L is continuous and
A12: for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ; ::_thesis: L is algebraic
now__::_thesis:_for_x_being_Element_of_L_holds_x_=_sup_(compactbelow_x)
let x be Element of L; ::_thesis: x = sup (compactbelow x)
A13: now__::_thesis:_for_z_being_Element_of_L_holds_
(_(_z_is_>=_than_waybelow_x_implies_z_is_>=_than_compactbelow_x_)_&_(_z_is_>=_than_compactbelow_x_implies_z_is_>=_than_waybelow_x_)_)
let z be Element of L; ::_thesis: ( ( z is_>=_than waybelow x implies z is_>=_than compactbelow x ) & ( z is_>=_than compactbelow x implies z is_>=_than waybelow x ) )
thus  ( z is_>=_than waybelow x implies z is_>=_than compactbelow x ) ::_thesis: ( z is_>=_than compactbelow x implies z is_>=_than waybelow x )
proof
assume A14: z is_>=_than waybelow x ; ::_thesis: z is_>=_than compactbelow x
now__::_thesis:_for_d_being_Element_of_L_st_d_in_compactbelow_x_holds_
d_<=_z
let d be Element of L; ::_thesis: ( d in compactbelow x implies d <= z )
assume A15: d in compactbelow x ; ::_thesis: d <= z
then  d is compact by Th4;
then A16: d << d by WAYBEL_3:def_2;
 d <= x by A15, Th4;
then  d << x by A16, WAYBEL_3:2;
then  d in waybelow x by WAYBEL_3:7;
hence  d <= z by A14, LATTICE3:def_9; ::_thesis: verum
end;
hence  z is_>=_than compactbelow x by LATTICE3:def_9; ::_thesis: verum
end;
thus  ( z is_>=_than compactbelow x implies z is_>=_than waybelow x ) ::_thesis: verum
proof
assume A17: z is_>=_than compactbelow x ; ::_thesis: z is_>=_than waybelow x
now__::_thesis:_for_d_being_Element_of_L_st_d_in_waybelow_x_holds_
d_<=_z
let d be Element of L; ::_thesis: ( d in waybelow x implies d <= z )
assume  d in waybelow x ; ::_thesis: d <= z
then  d << x by WAYBEL_3:7;
then consider k being Element of L such that
A18: k in the carrier of (CompactSublatt L) and
A19: d <= k and
A20: k <= x by A12;
 k is compact by A18, Def1;
then  k in compactbelow x by A20;
then  k <= z by A17, LATTICE3:def_9;
hence  d <= z by A19, ORDERS_2:3; ::_thesis: verum
end;
hence  z is_>=_than waybelow x by LATTICE3:def_9; ::_thesis: verum
end;
end;
 ( x = sup (waybelow x) & ex_sup_of waybelow x,L ) by A11, WAYBEL_0:75, WAYBEL_3:def_5;
hence  x = sup (compactbelow x) by A13, YELLOW_0:47; ::_thesis: verum
end;
then A21: L is satisfying_axiom_K by Def3;
 for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed )
proof
let x be Element of L; ::_thesis: ( not compactbelow x is empty & compactbelow x is directed )
now__::_thesis:_for_Y_being_finite_Subset_of_(compactbelow_x)_ex_c_being_Element_of_L_st_
(_c_in_compactbelow_x_&_c_is_>=_than_Y_)
let Y be finite Subset of (compactbelow x); ::_thesis: ex c being Element of L st
( c in compactbelow x & c is_>=_than Y )
 compactbelow x c= waybelow x by Th6;
then  Y is finite Subset of (waybelow x) by XBOOLE_1:1;
then consider b being Element of L such that
A22: b in waybelow x and
A23: b is_>=_than Y by A11, WAYBEL_0:1;
 b << x by A22, WAYBEL_3:7;
then consider c being Element of L such that
A24: c in the carrier of (CompactSublatt L) and
A25: b <= c and
A26: c <= x by A12;
take c = c; ::_thesis: ( c in compactbelow x & c is_>=_than Y )
 c is compact by A24, Def1;
hence  c in compactbelow x by A26; ::_thesis: c is_>=_than Y
thus  c is_>=_than Y by A23, A25, YELLOW_0:4; ::_thesis: verum
end;
hence  ( not compactbelow x is empty & compactbelow x is directed ) by WAYBEL_0:1; ::_thesis: verum
end;
hence  L is algebraic by A11, A21, Def4; ::_thesis: verum
end;

registration
cluster reflexive transitive antisymmetric with_suprema with_infima algebraic  ->  continuous for RelStr ;
coherence
 for b1 being LATTICE st b1 is algebraic holds
b1 is continuous by Th7;
end;

registration
cluster non empty reflexive algebraic  ->  non empty reflexive up-complete satisfying_axiom_K for RelStr ;
coherence
 for b1 being non empty reflexive RelStr st b1 is algebraic holds
( b1 is up-complete & b1 is satisfying_axiom_K ) by Def4;
end;

registration
let L be non empty with_suprema Poset;
cluster CompactSublatt L ->  strict full join-inheriting ;
coherence
 CompactSublatt L is join-inheriting
proof
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(CompactSublatt_L)_&_y_in_the_carrier_of_(CompactSublatt_L)_&_ex_sup_of_{x,y},L_holds_
sup_{x,y}_in_the_carrier_of_(CompactSublatt_L)
let x, y be Element of L; ::_thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_sup_of {x,y},L implies sup {x,y} in the carrier of (CompactSublatt L) )
assume that
A1: x in the carrier of (CompactSublatt L) and
A2: y in the carrier of (CompactSublatt L) and
A3: ex_sup_of {x,y},L ; ::_thesis: sup {x,y} in the carrier of (CompactSublatt L)
 y is compact by A2, Def1;
then A4: y << y by WAYBEL_3:def_2;
 x is compact by A1, Def1;
then A5: x << x by WAYBEL_3:def_2;
 y <= x "\/" y by A3, YELLOW_0:18;
then A6: y << x "\/" y by A4, WAYBEL_3:2;
 x <= x "\/" y by A3, YELLOW_0:18;
then  x << x "\/" y by A5, WAYBEL_3:2;
then  x "\/" y << x "\/" y by A6, WAYBEL_3:3;
then  x "\/" y is compact by WAYBEL_3:def_2;
then  sup {x,y} is compact by YELLOW_0:41;
hence  sup {x,y} in the carrier of (CompactSublatt L) by Def1; ::_thesis: verum
end;
hence  CompactSublatt L is join-inheriting by YELLOW_0:def_17; ::_thesis: verum
end;
end;

definition
let L be non empty reflexive RelStr ;
attrL is arithmetic  means :Def5: :: WAYBEL_8:def 5
( L is algebraic & CompactSublatt L is meet-inheriting );
end;

:: deftheorem Def5 defines arithmetic WAYBEL_8:def_5_:_
 for L being non empty reflexive RelStr holds
( L is arithmetic iff ( L is algebraic & CompactSublatt L is meet-inheriting ) );

begin

registration
cluster reflexive transitive antisymmetric with_suprema with_infima arithmetic  ->  algebraic for RelStr ;
coherence
 for b1 being LATTICE st b1 is arithmetic holds
b1 is algebraic by Def5;
end;

registration
cluster trivial reflexive transitive antisymmetric with_suprema with_infima  ->  arithmetic for RelStr ;
coherence
 for b1 being LATTICE st b1 is trivial holds
b1 is arithmetic
proof
let L be LATTICE; ::_thesis: ( L is trivial implies L is arithmetic )
assume A1: L is trivial ; ::_thesis: L is arithmetic
reconsider L9 = L as 1 -element LATTICE by A1;
A2: for x, y being Element of L9 st x << y holds
ex k being Element of L9 st
( k in the carrier of (CompactSublatt L9) & x <= k & k <= y )
proof
let x, y be Element of L9; ::_thesis: ( x << y implies ex k being Element of L9 st
( k in the carrier of (CompactSublatt L9) & x <= k & k <= y ) )
assume A3: x << y ; ::_thesis: ex k being Element of L9 st
( k in the carrier of (CompactSublatt L9) & x <= k & k <= y )
take k = x; ::_thesis: ( k in the carrier of (CompactSublatt L9) & x <= k & k <= y )
 x = y by STRUCT_0:def_10;
then  k is compact by A3, WAYBEL_3:def_2;
hence  k in the carrier of (CompactSublatt L9) by Def1; ::_thesis: ( x <= k & k <= y )
thus  ( x <= k & k <= y ) by STRUCT_0:def_10; ::_thesis: verum
end;
A4: L9 is algebraic by Th7, A2;
 for z, v being Element of L9 st z in the carrier of (CompactSublatt L9) & v in the carrier of (CompactSublatt L9) & ex_inf_of {z,v},L9 holds
inf {z,v} in the carrier of (CompactSublatt L9) by STRUCT_0:def_10;
then  CompactSublatt L9 is meet-inheriting by YELLOW_0:def_16;
hence  L is arithmetic by A4, Def5; ::_thesis: verum
end;
end;

registration
cluster non empty 1 -element strict reflexive transitive antisymmetric with_suprema with_infima for RelStr ;
existence
 ex b1 being LATTICE st
( b1 is 1 -element & b1 is strict )
proof
set B = the 1 -element strict reflexive RelStr ;
take  the 1 -element strict reflexive RelStr ; ::_thesis: ( the 1 -element strict reflexive RelStr is 1 -element & the 1 -element strict reflexive RelStr is strict )
thus  ( the 1 -element strict reflexive RelStr is 1 -element & the 1 -element strict reflexive RelStr is strict ) ; ::_thesis: verum
end;
end;

theorem Th8: :: WAYBEL_8:8
for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
for x1, y1 being Element of L1
for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2
proof
let L1, L2 be non empty reflexive antisymmetric RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete implies for x1, y1 being Element of L1
for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2 )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is up-complete ; ::_thesis: for x1, y1 being Element of L1
for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2
let x1, y1 be Element of L1; ::_thesis: for x2, y2 being Element of L2 st x1 = x2 & y1 = y2 & x1 << y1 holds
x2 << y2
let x2, y2 be Element of L2; ::_thesis: ( x1 = x2 & y1 = y2 & x1 << y1 implies x2 << y2 )
assume that
A3: x1 = x2 and
A4: y1 = y2 and
A5: x1 << y1 ; ::_thesis: x2 << y2
now__::_thesis:_for_D2_being_non_empty_directed_Subset_of_L2_st_y2_<=_sup_D2_holds_
ex_d2_being_Element_of_L2_st_
(_d2_in_D2_&_x2_<=_d2_)
let D2 be non empty directed Subset of L2; ::_thesis: ( y2 <= sup D2 implies ex d2 being Element of L2 st
( d2 in D2 & x2 <= d2 ) )
reconsider D1 = D2 as Subset of L1 by A1;
reconsider D1 = D1 as non empty directed Subset of L1 by A1, WAYBEL_0:3;
 ex_sup_of D1,L1 by A2, WAYBEL_0:75;
then A6: sup D1 = sup D2 by A1, YELLOW_0:26;
assume  y2 <= sup D2 ; ::_thesis: ex d2 being Element of L2 st
( d2 in D2 & x2 <= d2 )
then  y1 <= sup D1 by A1, A4, A6, YELLOW_0:1;
then consider d1 being Element of L1 such that
A7: d1 in D1 and
A8: x1 <= d1 by A5, WAYBEL_3:def_1;
reconsider d2 = d1 as Element of L2 by A1;
take d2 = d2; ::_thesis: ( d2 in D2 & x2 <= d2 )
thus  d2 in D2 by A7; ::_thesis: x2 <= d2
thus  x2 <= d2 by A1, A3, A8, YELLOW_0:1; ::_thesis: verum
end;
hence  x2 << y2 by WAYBEL_3:def_1; ::_thesis: verum
end;

theorem Th9: :: WAYBEL_8:9
for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
for x being Element of L1
for y being Element of L2 st x = y & x is compact holds
y is compact
proof
let L1, L2 be non empty reflexive antisymmetric RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete implies for x being Element of L1
for y being Element of L2 st x = y & x is compact holds
y is compact )
assume A1: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete ) ; ::_thesis: for x being Element of L1
for y being Element of L2 st x = y & x is compact holds
y is compact
let x be Element of L1; ::_thesis: for y being Element of L2 st x = y & x is compact holds
y is compact
let y be Element of L2; ::_thesis: ( x = y & x is compact implies y is compact )
assume that
A2: x = y and
A3: x is compact ; ::_thesis: y is compact
 x << x by A3, WAYBEL_3:def_2;
then  y << y by A1, A2, Th8;
hence  y is compact by WAYBEL_3:def_2; ::_thesis: verum
end;

theorem Th10: :: WAYBEL_8:10
for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for x being Element of L1
for y being Element of L2 st x = y holds
compactbelow x = compactbelow y
proof
let L1, L2 be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for x being Element of L1
for y being Element of L2 st x = y holds
compactbelow x = compactbelow y )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for x being Element of L1
for y being Element of L2 st x = y holds
compactbelow x = compactbelow y
let x be Element of L1; ::_thesis: for y being Element of L2 st x = y holds
compactbelow x = compactbelow y
let y be Element of L2; ::_thesis: ( x = y implies compactbelow x = compactbelow y )
assume A2: x = y ; ::_thesis: compactbelow x = compactbelow y
now__::_thesis:_for_z_being_set_st_z_in_compactbelow_y_holds_
z_in_compactbelow_x
let z be set ; ::_thesis: ( z in compactbelow y implies z in compactbelow x )
assume A3: z in compactbelow y ; ::_thesis: z in compactbelow x
then reconsider z2 = z as Element of L2 ;
reconsider z1 = z2 as Element of L1 by A1;
 z2 is compact by A3, Th4;
then A4: z1 is compact by A1, Th9;
 z2 <= y by A3, Th4;
then  z1 <= x by A1, A2, YELLOW_0:1;
hence  z in compactbelow x by A4; ::_thesis: verum
end;
then A5: compactbelow y c= compactbelow x by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_compactbelow_x_holds_
z_in_compactbelow_y
let z be set ; ::_thesis: ( z in compactbelow x implies z in compactbelow y )
assume A6: z in compactbelow x ; ::_thesis: z in compactbelow y
then reconsider z1 = z as Element of L1 ;
reconsider z2 = z1 as Element of L2 by A1;
 z1 is compact by A6, Th4;
then A7: z2 is compact by A1, Th9;
 z1 <= x by A6, Th4;
then  z2 <= y by A1, A2, YELLOW_0:1;
hence  z in compactbelow y by A7; ::_thesis: verum
end;
then  compactbelow x c= compactbelow y by TARSKI:def_3;
hence  compactbelow x = compactbelow y by A5, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: WAYBEL_8:11
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & not L1 is empty holds
not L2 is empty ;

theorem Th12: :: WAYBEL_8:12
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is reflexive holds
L2 is reflexive
proof
let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is reflexive implies L2 is reflexive )
assume A1: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & the InternalRel of L1 is_reflexive_in the carrier of L1 ) ; :: according to ORDERS_2:def_2 ::_thesis: L2 is reflexive
let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of L2 or [x,x] in the InternalRel of L2 )
assume  x in the carrier of L2 ; ::_thesis: [x,x] in the InternalRel of L2
hence  [x,x] in the InternalRel of L2 by A1, RELAT_2:def_1; ::_thesis: verum
end;

theorem Th13: :: WAYBEL_8:13
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is transitive holds
L2 is transitive
proof
let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is transitive implies L2 is transitive )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is transitive ; ::_thesis: L2 is transitive
now__::_thesis:_for_x,_y,_z_being_Element_of_L2_st_x_<=_y_&_y_<=_z_holds_
x_<=_z
let x, y, z be Element of L2; ::_thesis: ( x <= y & y <= z implies x <= z )
reconsider x9 = x, y9 = y, z9 = z as Element of L1 by A1;
assume  ( x <= y & y <= z ) ; ::_thesis: x <= z
then  ( x9 <= y9 & y9 <= z9 ) by A1, YELLOW_0:1;
then  x9 <= z9 by A2, YELLOW_0:def_2;
hence  x <= z by A1, YELLOW_0:1; ::_thesis: verum
end;
hence  L2 is transitive by YELLOW_0:def_2; ::_thesis: verum
end;

theorem Th14: :: WAYBEL_8:14
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is antisymmetric holds
L2 is antisymmetric
proof
let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is antisymmetric implies L2 is antisymmetric )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is antisymmetric ; ::_thesis: L2 is antisymmetric
now__::_thesis:_for_x,_y_being_Element_of_L2_st_x_<=_y_&_y_<=_x_holds_
x_=_y
let x, y be Element of L2; ::_thesis: ( x <= y & y <= x implies x = y )
reconsider x9 = x, y9 = y as Element of L1 by A1;
assume  ( x <= y & y <= x ) ; ::_thesis: x = y
then  ( x9 <= y9 & y9 <= x9 ) by A1, YELLOW_0:1;
hence  x = y by A2, YELLOW_0:def_3; ::_thesis: verum
end;
hence  L2 is antisymmetric by YELLOW_0:def_3; ::_thesis: verum
end;

theorem Th15: :: WAYBEL_8:15
for L1, L2 being non empty reflexive RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
L2 is up-complete
proof
let L1, L2 be non empty reflexive RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete implies L2 is up-complete )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is up-complete ; ::_thesis: L2 is up-complete
now__::_thesis:_for_X_being_non_empty_directed_Subset_of_L2_ex_x_being_Element_of_L2_st_
(_x_is_>=_than_X_&_(_for_y_being_Element_of_L2_st_y_is_>=_than_X_holds_
x_<=_y_)_)
let X be non empty directed Subset of L2; ::_thesis: ex x being Element of L2 st
( x is_>=_than X & ( for y being Element of L2 st y is_>=_than X holds
x <= y ) )
reconsider X9 = X as Subset of L1 by A1;
reconsider X9 = X9 as non empty directed Subset of L1 by A1, WAYBEL_0:3;
consider x9 being Element of L1 such that
A3: x9 is_>=_than X9 and
A4: for y9 being Element of L1 st y9 is_>=_than X9 holds
x9 <= y9 by A2, WAYBEL_0:def_39;
reconsider x = x9 as Element of L2 by A1;
take x = x; ::_thesis: ( x is_>=_than X & ( for y being Element of L2 st y is_>=_than X holds
x <= y ) )
thus  x is_>=_than X by A1, A3, YELLOW_0:2; ::_thesis: for y being Element of L2 st y is_>=_than X holds
x <= y
let y be Element of L2; ::_thesis: ( y is_>=_than X implies x <= y )
assume A5: y is_>=_than X ; ::_thesis: x <= y
reconsider y9 = y as Element of L1 by A1;
 x9 <= y9 by A1, A4, A5, YELLOW_0:2;
hence  x <= y by A1, YELLOW_0:1; ::_thesis: verum
end;
hence  L2 is up-complete by WAYBEL_0:def_39; ::_thesis: verum
end;

theorem Th16: :: WAYBEL_8:16
for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is satisfying_axiom_K & ( for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ) holds
L2 is satisfying_axiom_K
proof
let L1, L2 be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is satisfying_axiom_K & ( for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ) implies L2 is satisfying_axiom_K )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is satisfying_axiom_K and
A3: for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ; ::_thesis: L2 is satisfying_axiom_K
now__::_thesis:_for_x_being_Element_of_L2_holds_x_=_sup_(compactbelow_x)
let x be Element of L2; ::_thesis: x = sup (compactbelow x)
reconsider x9 = x as Element of L1 by A1;
 ( not compactbelow x9 is empty & compactbelow x9 is directed ) by A3;
then A4: ex_sup_of compactbelow x9,L1 by WAYBEL_0:75;
 ( x9 = sup (compactbelow x9) & compactbelow x = compactbelow x9 ) by A1, A2, Def3, Th10;
hence  x = sup (compactbelow x) by A1, A4, YELLOW_0:26; ::_thesis: verum
end;
hence  L2 is satisfying_axiom_K by Def3; ::_thesis: verum
end;

theorem Th17: :: WAYBEL_8:17
for L1, L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is algebraic holds
L2 is algebraic
proof
let L1, L2 be non empty reflexive antisymmetric RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is algebraic implies L2 is algebraic )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is algebraic ; ::_thesis: L2 is algebraic
A3: L2 is up-complete by A1, A2, Th15;
A4: for x being Element of L2 holds
( not compactbelow x is empty & compactbelow x is directed )
proof
let x be Element of L2; ::_thesis: ( not compactbelow x is empty & compactbelow x is directed )
reconsider x9 = x as Element of L1 by A1;
 ( not compactbelow x9 is empty & compactbelow x9 is directed ) by A2, Def4;
hence  ( not compactbelow x is empty & compactbelow x is directed ) by A1, A2, A3, Th10, WAYBEL_0:3; ::_thesis: verum
end;
 for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) by A2, Def4;
then  L2 is satisfying_axiom_K by A1, A2, A3, Th16;
hence  L2 is algebraic by A3, A4, Def4; ::_thesis: verum
end;

theorem Th18: :: WAYBEL_8:18
for L1, L2 being LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is arithmetic holds
L2 is arithmetic
proof
let L1, L2 be LATTICE; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is arithmetic implies L2 is arithmetic )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is arithmetic ; ::_thesis: L2 is arithmetic
A3: L2 is algebraic by A1, A2, Th17;
A4: CompactSublatt L1 is meet-inheriting by A2, Def5;
now__::_thesis:_for_x2,_y2_being_Element_of_L2_st_x2_in_the_carrier_of_(CompactSublatt_L2)_&_y2_in_the_carrier_of_(CompactSublatt_L2)_&_ex_inf_of_{x2,y2},L2_holds_
inf_{x2,y2}_in_the_carrier_of_(CompactSublatt_L2)
let x2, y2 be Element of L2; ::_thesis: ( x2 in the carrier of (CompactSublatt L2) & y2 in the carrier of (CompactSublatt L2) & ex_inf_of {x2,y2},L2 implies inf {x2,y2} in the carrier of (CompactSublatt L2) )
reconsider x1 = x2, y1 = y2 as Element of L1 by A1;
assume that
A5: x2 in the carrier of (CompactSublatt L2) and
A6: y2 in the carrier of (CompactSublatt L2) and
A7: ex_inf_of {x2,y2},L2 ; ::_thesis: inf {x2,y2} in the carrier of (CompactSublatt L2)
 x2 is compact by A5, Def1;
then  x1 is compact by A1, A3, Th9;
then A8: x1 in the carrier of (CompactSublatt L1) by Def1;
 y2 is compact by A6, Def1;
then  y1 is compact by A1, A3, Th9;
then A9: y1 in the carrier of (CompactSublatt L1) by Def1;
 ex_inf_of {x1,y1},L1 by A1, A7, YELLOW_0:14;
then  inf {x1,y1} in the carrier of (CompactSublatt L1) by A4, A8, A9, YELLOW_0:def_16;
then A10: inf {x1,y1} is compact by Def1;
 inf {x1,y1} = inf {x2,y2} by A1, A7, YELLOW_0:27;
then  inf {x2,y2} is compact by A1, A2, A10, Th9;
hence  inf {x2,y2} in the carrier of (CompactSublatt L2) by Def1; ::_thesis: verum
end;
then  CompactSublatt L2 is meet-inheriting by YELLOW_0:def_16;
hence  L2 is arithmetic by A3, Def5; ::_thesis: verum
end;

registration
let L be non empty RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) ->  non empty ;
coherence
 not RelStr(# the carrier of L, the InternalRel of L #) is empty ;
end;

registration
let L be non empty reflexive RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) ->  reflexive ;
coherence
 RelStr(# the carrier of L, the InternalRel of L #) is reflexive by Th12;
end;

registration
let L be transitive RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) ->  transitive ;
coherence
 RelStr(# the carrier of L, the InternalRel of L #) is transitive by Th13;
end;

registration
let L be antisymmetric RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) ->  antisymmetric ;
coherence
 RelStr(# the carrier of L, the InternalRel of L #) is antisymmetric by Th14;
end;

registration
let L be with_infima RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) ->  with_infima ;
coherence
 RelStr(# the carrier of L, the InternalRel of L #) is with_infima by YELLOW_7:14;
end;

registration
let L be with_suprema RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) ->  with_suprema ;
coherence
 RelStr(# the carrier of L, the InternalRel of L #) is with_suprema by YELLOW_7:15;
end;

registration
let L be non empty reflexive up-complete RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) ->  up-complete ;
coherence
 RelStr(# the carrier of L, the InternalRel of L #) is up-complete by Th15;
end;

registration
let L be non empty reflexive antisymmetric algebraic RelStr ;
cluster RelStr(# the carrier of L, the InternalRel of L #) ->  algebraic ;
coherence
 RelStr(# the carrier of L, the InternalRel of L #) is algebraic by Th17;
end;

registration
let L be arithmetic LATTICE;
cluster RelStr(# the carrier of L, the InternalRel of L #) ->  arithmetic ;
coherence
 RelStr(# the carrier of L, the InternalRel of L #) is arithmetic by Th18;
end;

theorem :: WAYBEL_8:19
for L being algebraic LATTICE holds
( L is arithmetic iff CompactSublatt L is LATTICE )
proof
let L be algebraic LATTICE; ::_thesis: ( L is arithmetic iff CompactSublatt L is LATTICE )
thus  ( L is arithmetic implies CompactSublatt L is LATTICE ) ::_thesis: ( CompactSublatt L is LATTICE implies L is arithmetic )
proof
set x = the Element of L;
assume A1: L is arithmetic ; ::_thesis: CompactSublatt L is LATTICE
 not compactbelow the Element of L is empty by Def4;
then consider z being set  such that
A2: z in compactbelow the Element of L by XBOOLE_0:def_1;
 ex z9 being Element of L st
( z9 = z & the Element of L >= z9 & z9 is compact ) by A2;
then  CompactSublatt L is non empty full meet-inheriting join-inheriting SubRelStr of L by A1, Def1, Def5;
hence  CompactSublatt L is LATTICE ; ::_thesis: verum
end;
assume A3: CompactSublatt L is LATTICE ; ::_thesis: L is arithmetic
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(CompactSublatt_L)_&_y_in_the_carrier_of_(CompactSublatt_L)_&_ex_inf_of_{x,y},L_holds_
inf_{x,y}_in_the_carrier_of_(CompactSublatt_L)
let x, y be Element of L; ::_thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (CompactSublatt L) )
assume that
A4: x in the carrier of (CompactSublatt L) and
A5: y in the carrier of (CompactSublatt L) and
 ex_inf_of {x,y},L ; ::_thesis: inf {x,y} in the carrier of (CompactSublatt L)
reconsider L9 = CompactSublatt L as non empty full SubRelStr of L by A4;
reconsider x9 = x, y9 = y as Element of L9 by A4, A5;
set X = compactbelow (inf {x,y});
reconsider c = "/\" ({x,y},L9) as Element of L by YELLOW_0:58;
A6: inf {x,y} = sup (compactbelow (inf {x,y})) by Def3;
 ( not compactbelow (inf {x,y}) is empty & compactbelow (inf {x,y}) is directed ) by Def4;
then A7: ex_sup_of compactbelow (inf {x,y}),L by WAYBEL_0:75;
A8: ex_inf_of {x9,y9},L9 by A3, YELLOW_0:21;
then A9: "/\" ({x,y},L9) is_<=_than {x,y} by YELLOW_0:31;
now__::_thesis:_for_z_being_set_st_z_in_compactbelow_(inf_{x,y})_holds_
z_in_(compactbelow_x)_/\_(compactbelow_y)
let z be set ; ::_thesis: ( z in compactbelow (inf {x,y}) implies z in (compactbelow x) /\ (compactbelow y) )
assume  z in compactbelow (inf {x,y}) ; ::_thesis: z in (compactbelow x) /\ (compactbelow y)
then consider z1 being Element of L such that
A10: z = z1 and
A11: inf {x,y} >= z1 and
A12: z1 is compact ;
A13: z1 <= x "/\" y by A11, YELLOW_0:40;
 x "/\" y <= y by YELLOW_0:23;
then  z1 <= y by A13, ORDERS_2:3;
then A14: z in compactbelow y by A10, A12;
 x "/\" y <= x by YELLOW_0:23;
then  z1 <= x by A13, ORDERS_2:3;
then  z in compactbelow x by A10, A12;
hence  z in (compactbelow x) /\ (compactbelow y) by A14, XBOOLE_0:def_4; ::_thesis: verum
end;
then A15: compactbelow (inf {x,y}) c= (compactbelow x) /\ (compactbelow y) by TARSKI:def_3;
now__::_thesis:_for_b9_being_Element_of_L9_st_b9_in_compactbelow_(inf_{x,y})_holds_
b9_<=_"/\"_({x,y},L9)
let b9 be Element of L9; ::_thesis: ( b9 in compactbelow (inf {x,y}) implies b9 <= "/\" ({x,y},L9) )
reconsider b = b9 as Element of L by YELLOW_0:58;
assume A16: b9 in compactbelow (inf {x,y}) ; ::_thesis: b9 <= "/\" ({x,y},L9)
then  b9 in compactbelow y by A15, XBOOLE_0:def_4;
then  b <= y by Th4;
then A17: b9 <= y9 by YELLOW_0:60;
 b9 in compactbelow x by A15, A16, XBOOLE_0:def_4;
then  b <= x by Th4;
then  b9 <= x9 by YELLOW_0:60;
then  b9 <= x9 "/\" y9 by A8, A17, YELLOW_0:19;
hence  b9 <= "/\" ({x,y},L9) by A3, YELLOW_0:40; ::_thesis: verum
end;
then A18: compactbelow (inf {x,y}) is_<=_than "/\" ({x,y},L9) by LATTICE3:def_9;
now__::_thesis:_for_d_being_set_st_d_in_compactbelow_(inf_{x,y})_holds_
d_in_the_carrier_of_L9
let d be set ; ::_thesis: ( d in compactbelow (inf {x,y}) implies d in the carrier of L9 )
assume  d in compactbelow (inf {x,y}) ; ::_thesis: d in the carrier of L9
then  ex d9 being Element of L st
( d9 = d & inf {x,y} >= d9 & d9 is compact ) ;
hence  d in the carrier of L9 by Def1; ::_thesis: verum
end;
then  compactbelow (inf {x,y}) c= the carrier of L9 by TARSKI:def_3;
then  compactbelow (inf {x,y}) is_<=_than c by A18, YELLOW_0:62;
then A19: sup (compactbelow (inf {x,y})) <= c by A7, YELLOW_0:30;
 y9 in {x,y} by TARSKI:def_2;
then  "/\" ({x,y},L9) <= y9 by A9, LATTICE3:def_8;
then A20: c <= y by YELLOW_0:59;
 x9 in {x,y} by TARSKI:def_2;
then  "/\" ({x,y},L9) <= x9 by A9, LATTICE3:def_8;
then  c <= x by YELLOW_0:59;
then  c <= x "/\" y by A20, YELLOW_0:23;
then  c <= sup (compactbelow (inf {x,y})) by A6, YELLOW_0:40;
then  c = sup (compactbelow (inf {x,y})) by A19, ORDERS_2:2;
hence  inf {x,y} in the carrier of (CompactSublatt L) by A6; ::_thesis: verum
end;
then  CompactSublatt L is meet-inheriting by YELLOW_0:def_16;
hence  L is arithmetic by Def5; ::_thesis: verum
end;

theorem Th20: :: WAYBEL_8:20
for L being lower-bounded algebraic LATTICE holds
( L is arithmetic iff L -waybelow is multiplicative )
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: ( L is arithmetic iff L -waybelow is multiplicative )
thus  ( L is arithmetic implies L -waybelow is multiplicative ) ::_thesis: ( L -waybelow is multiplicative implies L is arithmetic )
proof
assume A1: L is arithmetic ; ::_thesis: L -waybelow is multiplicative
now__::_thesis:_for_a,_x,_y_being_Element_of_L_st_[a,x]_in_L_-waybelow_&_[a,y]_in_L_-waybelow_holds_
[a,(x_"/\"_y)]_in_L_-waybelow
reconsider C = CompactSublatt L as non empty full meet-inheriting SubRelStr of L by A1, Def5;
let a, x, y be Element of L; ::_thesis: ( [a,x] in L -waybelow & [a,y] in L -waybelow implies [a,(x "/\" y)] in L -waybelow )
assume that
A2: [a,x] in L -waybelow and
A3: [a,y] in L -waybelow ; ::_thesis: [a,(x "/\" y)] in L -waybelow
 a << x by A2, WAYBEL_4:def_1;
then consider c being Element of L such that
A4: c in the carrier of (CompactSublatt L) and
A5: a <= c and
A6: c <= x by Th7;
 a << y by A3, WAYBEL_4:def_1;
then consider k being Element of L such that
A7: k in the carrier of (CompactSublatt L) and
A8: a <= k and
A9: k <= y by Th7;
A10: c "/\" k <= x "/\" y by A6, A9, YELLOW_3:2;
reconsider c9 = c, k9 = k as Element of C by A4, A7;
 c9 "/\" k9 in the carrier of (CompactSublatt L) ;
then  c "/\" k in the carrier of (CompactSublatt L) by YELLOW_0:69;
then  c "/\" k is compact by Def1;
then A11: c "/\" k << c "/\" k by WAYBEL_3:def_2;
 a "/\" a = a by YELLOW_5:2;
then  a <= c "/\" k by A5, A8, YELLOW_3:2;
then  a << x "/\" y by A10, A11, WAYBEL_3:2;
hence  [a,(x "/\" y)] in L -waybelow by WAYBEL_4:def_1; ::_thesis: verum
end;
hence  L -waybelow is multiplicative by WAYBEL_7:def_7; ::_thesis: verum
end;
assume A12: L -waybelow is multiplicative ; ::_thesis: L is arithmetic
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_the_carrier_of_(CompactSublatt_L)_&_y_in_the_carrier_of_(CompactSublatt_L)_&_ex_inf_of_{x,y},L_holds_
inf_{x,y}_in_the_carrier_of_(CompactSublatt_L)
let x, y be Element of L; ::_thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_inf_of {x,y},L implies inf {x,y} in the carrier of (CompactSublatt L) )
assume that
A13: x in the carrier of (CompactSublatt L) and
A14: y in the carrier of (CompactSublatt L) and
 ex_inf_of {x,y},L ; ::_thesis: inf {x,y} in the carrier of (CompactSublatt L)
 y is compact by A14, Def1;
then  y << y by WAYBEL_3:def_2;
then A15: [y,y] in L -waybelow by WAYBEL_4:def_1;
 x is compact by A13, Def1;
then  x << x by WAYBEL_3:def_2;
then  [x,x] in L -waybelow by WAYBEL_4:def_1;
then  [(x "/\" y),(x "/\" y)] in L -waybelow by A12, A15, WAYBEL_7:41;
then  x "/\" y << x "/\" y by WAYBEL_4:def_1;
then  x "/\" y is compact by WAYBEL_3:def_2;
then  x "/\" y in the carrier of (CompactSublatt L) by Def1;
hence  inf {x,y} in the carrier of (CompactSublatt L) by YELLOW_0:40; ::_thesis: verum
end;
then  CompactSublatt L is meet-inheriting by YELLOW_0:def_16;
hence  L is arithmetic by Def5; ::_thesis: verum
end;

theorem :: WAYBEL_8:21
for L being lower-bounded arithmetic LATTICE
for p being Element of L st p is pseudoprime holds
p is prime
proof
let L be lower-bounded arithmetic LATTICE; ::_thesis: for p being Element of L st p is pseudoprime holds
p is prime
let p be Element of L; ::_thesis: ( p is pseudoprime implies p is prime )
 L -waybelow is multiplicative by Th20;
hence  ( p is pseudoprime implies p is prime ) by WAYBEL_7:45; ::_thesis: verum
end;

theorem :: WAYBEL_8:22
for L being lower-bounded distributive algebraic LATTICE st ( for p being Element of L st p is pseudoprime holds
p is prime ) holds
L is arithmetic
proof
let L be lower-bounded distributive algebraic LATTICE; ::_thesis: ( ( for p being Element of L st p is pseudoprime holds
p is prime ) implies L is arithmetic )
assume  for p being Element of L st p is pseudoprime holds
p is prime ; ::_thesis: L is arithmetic
then  L -waybelow is multiplicative by WAYBEL_7:46;
hence  L is arithmetic by Th20; ::_thesis: verum
end;

registration
let L be algebraic LATTICE;
let c be closure Function of L,L;
cluster non empty directed for Element of bool the carrier of (Image c);
existence
 ex b1 being Subset of (Image c) st
( not b1 is empty & b1 is directed )
proof
set x = the Element of (Image c);
take  downarrow the Element of (Image c) ; ::_thesis: ( not downarrow the Element of (Image c) is empty & downarrow the Element of (Image c) is directed )
thus  ( not downarrow the Element of (Image c) is empty & downarrow the Element of (Image c) is directed ) ; ::_thesis: verum
end;
end;

theorem Th23: :: WAYBEL_8:23
for L being algebraic LATTICE
for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))
proof
let L be algebraic LATTICE; ::_thesis: for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))
let c be closure Function of L,L; ::_thesis: ( c is directed-sups-preserving implies c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) )
assume A1: c is directed-sups-preserving ; ::_thesis: c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in c .: ([#] (CompactSublatt L)) or x in [#] (CompactSublatt (Image c)) )
A2: ( c is idempotent & c is monotone ) by WAYBEL_1:def_13;
assume  x in c .: ([#] (CompactSublatt L)) ; ::_thesis: x in [#] (CompactSublatt (Image c))
then consider y being set  such that
A3: y in dom c and
A4: y in [#] (CompactSublatt L) and
A5: x = c . y by FUNCT_1:def_6;
A6: x in rng c by A3, A5, FUNCT_1:def_3;
then reconsider x9 = x as Element of (Image c) by YELLOW_0:def_15;
reconsider x1 = x9 as Element of L by A6;
reconsider y9 = y as Element of L by A3;
 y9 is compact by A4, Def1;
then A7: y9 << y9 by WAYBEL_3:def_2;
now__::_thesis:_for_D_being_non_empty_directed_Subset_of_(Image_c)_st_x9_<=_sup_D_holds_
ex_d_being_Element_of_(Image_c)_st_
(_d_in_D_&_x9_<=_d_)
 id L <= c by WAYBEL_1:def_14;
then  (id L) . y9 <= c . y9 by YELLOW_2:9;
then A8: y9 <= x1 by A5, FUNCT_1:18;
let D be non empty directed Subset of (Image c); ::_thesis: ( x9 <= sup D implies ex d being Element of (Image c) st
( d in D & x9 <= d ) )
assume A9: x9 <= sup D ; ::_thesis: ex d being Element of (Image c) st
( d in D & x9 <= d )
 D c= the carrier of (Image c) ;
then A10: D c= rng c by YELLOW_0:def_15;
then reconsider D9 = D as non empty Subset of L by XBOOLE_1:1;
reconsider D9 = D9 as non empty directed Subset of L by YELLOW_2:7;
A11: ex_sup_of D9,L by WAYBEL_0:75;
 c preserves_sup_of D9 by A1, WAYBEL_0:def_37;
then A12: c . (sup D9) = sup (c .: D9) by A11, WAYBEL_0:def_31
.= sup D9 by A2, A10, YELLOW_2:20 ;
 c . (sup D9) = sup D by A11, WAYBEL_1:55;
then  x1 <= sup D9 by A9, A12, YELLOW_0:59;
then  y9 <= sup D9 by A8, ORDERS_2:3;
then consider d9 being Element of L such that
A13: d9 in D9 and
A14: y9 <= d9 by A7, WAYBEL_3:def_1;
reconsider d = d9 as Element of (Image c) by A13;
take d = d; ::_thesis: ( d in D & x9 <= d )
thus  d in D by A13; ::_thesis: x9 <= d
 d in the carrier of (Image c) ;
then  d in rng c by YELLOW_0:def_15;
then  d9 in  {  z where z is Element of L : z = c . z  }  by A2, YELLOW_2:19;
then A15: ex z9 being Element of L st
( d9 = z9 & z9 = c . z9 ) ;
 c . y9 <= c . d9 by A2, A14, WAYBEL_1:def_2;
hence  x9 <= d by A5, A15, YELLOW_0:60; ::_thesis: verum
end;
then  x9 << x9 by WAYBEL_3:def_1;
then  x9 is compact by WAYBEL_3:def_2;
hence  x in [#] (CompactSublatt (Image c)) by Def1; ::_thesis: verum
end;

theorem :: WAYBEL_8:24
for L being lower-bounded algebraic LATTICE
for c being closure Function of L,L st c is directed-sups-preserving holds
Image c is algebraic LATTICE
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: for c being closure Function of L,L st c is directed-sups-preserving holds
Image c is algebraic LATTICE
let c be closure Function of L,L; ::_thesis: ( c is directed-sups-preserving implies Image c is algebraic LATTICE )
assume A1: c is directed-sups-preserving ; ::_thesis: Image c is algebraic LATTICE
 c is idempotent by WAYBEL_1:def_13;
then reconsider Imc = Image c as complete LATTICE by A1, YELLOW_2:35;
A2: now__::_thesis:_for_x_being_Element_of_Imc_holds_
(_not_compactbelow_x_is_empty_&_compactbelow_x_is_directed_)
let x be Element of Imc; ::_thesis: ( not compactbelow x is empty & compactbelow x is directed )
now__::_thesis:_for_y,_z_being_Element_of_Imc_st_y_in_compactbelow_x_&_z_in_compactbelow_x_holds_
ex_v_being_Element_of_the_carrier_of_Imc_st_
(_v_in_compactbelow_x_&_y_<=_v_&_z_<=_v_)
let y, z be Element of Imc; ::_thesis: ( y in compactbelow x & z in compactbelow x implies ex v being Element of the carrier of Imc st
( v in compactbelow x & y <= v & z <= v ) )
assume that
A3: y in compactbelow x and
A4: z in compactbelow x ; ::_thesis: ex v being Element of the carrier of Imc st
( v in compactbelow x & y <= v & z <= v )
 y is compact by A3, Th4;
then A5: y << y by WAYBEL_3:def_2;
 z is compact by A4, Th4;
then A6: z << z by WAYBEL_3:def_2;
take v = y "\/" z; ::_thesis: ( v in compactbelow x & y <= v & z <= v )
 z <= v by YELLOW_0:22;
then A7: z << v by A6, WAYBEL_3:2;
 y <= v by YELLOW_0:22;
then  y << v by A5, WAYBEL_3:2;
then  v << v by A7, WAYBEL_3:3;
then A8: v is compact by WAYBEL_3:def_2;
 ( y <= x & z <= x ) by A3, A4, Th4;
then  v <= x by YELLOW_0:22;
hence  ( v in compactbelow x & y <= v & z <= v ) by A8, YELLOW_0:22; ::_thesis: verum
end;
hence  ( not compactbelow x is empty & compactbelow x is directed ) by WAYBEL_0:def_1; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Element_of_Imc_holds_x_=_sup_(compactbelow_x)
let x be Element of Imc; ::_thesis: x = sup (compactbelow x)
consider y being Element of L such that
A9: c . y = x by YELLOW_2:10;
 sup (compactbelow y) in the carrier of L ;
then A10: sup (compactbelow y) in dom c by FUNCT_2:def_1;
 ( not compactbelow y is empty & compactbelow y is directed ) by Def4;
then A11: ( c preserves_sup_of compactbelow y & ex_sup_of compactbelow y,L ) by A1, WAYBEL_0:75, WAYBEL_0:def_37;
then  c . (sup (compactbelow y)) = sup (c .: (compactbelow y)) by WAYBEL_0:def_31;
then  sup (c .: (compactbelow y)) in rng c by A10, FUNCT_1:def_3;
then A12: ( ex_sup_of c .: (compactbelow y),L & sup (c .: (compactbelow y)) in the carrier of (Image c) ) by YELLOW_0:17, YELLOW_0:def_15;
 for b being Element of Imc st b in compactbelow x holds
b <= x by Th4;
then  x is_>=_than compactbelow x by LATTICE3:def_9;
then A13: sup (compactbelow x) <= x by YELLOW_0:32;
A14: c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) by A1, Th23;
A15: c is monotone by A1, YELLOW_2:16;
 compactbelow y = (downarrow y) /\ ([#] (CompactSublatt L)) by Th5;
then A16: c .: (compactbelow y) c= (c .: (downarrow y)) /\ (c .: ([#] (CompactSublatt L))) by RELAT_1:121;
now__::_thesis:_for_z_being_set_st_z_in_c_.:_(compactbelow_y)_holds_
z_in_compactbelow_x
let z be set ; ::_thesis: ( z in c .: (compactbelow y) implies z in compactbelow x )
assume A17: z in c .: (compactbelow y) ; ::_thesis: z in compactbelow x
then consider v being set  such that
A18: v in dom c and
A19: v in compactbelow y and
A20: z = c . v by FUNCT_1:def_6;
 z in rng c by A18, A20, FUNCT_1:def_3;
then reconsider z1 = z as Element of Imc by YELLOW_0:def_15;
reconsider v = v as Element of L by A18;
 v <= y by A19, Th4;
then  c . v <= c . y by A15, WAYBEL_1:def_2;
then A21: z1 <= x by A9, A20, YELLOW_0:60;
 z in c .: ([#] (CompactSublatt L)) by A16, A17, XBOOLE_0:def_4;
then  z1 is compact by A14, Def1;
hence  z in compactbelow x by A21; ::_thesis: verum
end;
then A22: c .: (compactbelow y) c= compactbelow x by TARSKI:def_3;
 compactbelow x is directed by A2;
then A23: ex_sup_of compactbelow x,Imc by WAYBEL_0:75;
 c .: (compactbelow y) c= rng c by RELAT_1:111;
then  c .: (compactbelow y) is Subset of Imc by YELLOW_0:def_15;
then A24: ( ex_sup_of c .: (compactbelow y),Imc & sup (c .: (compactbelow y)) = "\/" ((c .: (compactbelow y)),Imc) ) by A12, YELLOW_0:64;
c . y = c . (sup (compactbelow y)) by Def3
.= sup (c .: (compactbelow y)) by A11, WAYBEL_0:def_31 ;
then  x <= sup (compactbelow x) by A9, A23, A24, A22, YELLOW_0:34;
hence  x = sup (compactbelow x) by A13, ORDERS_2:2; ::_thesis: verum
end;
then  Imc is satisfying_axiom_K by Def3;
hence  Image c is algebraic LATTICE by A2, Def4; ::_thesis: verum
end;

theorem :: WAYBEL_8:25
for L being lower-bounded algebraic LATTICE
for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))
let c be closure Function of L,L; ::_thesis: ( c is directed-sups-preserving implies c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c)) )
assume A1: c is directed-sups-preserving ; ::_thesis: c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))
now__::_thesis:_for_a9_being_set_st_a9_in_[#]_(CompactSublatt_(Image_c))_holds_
a9_in_c_.:_([#]_(CompactSublatt_L))
 c is idempotent by WAYBEL_1:def_13;
then A2: rng c =  {  x where x is Element of L : x = c . x  }  by YELLOW_2:19;
 c is idempotent by WAYBEL_1:def_13;
then reconsider Imc = Image c as complete LATTICE by A1, YELLOW_2:35;
let a9 be set ; ::_thesis: ( a9 in [#] (CompactSublatt (Image c)) implies a9 in c .: ([#] (CompactSublatt L)) )
assume A3: a9 in [#] (CompactSublatt (Image c)) ; ::_thesis: a9 in c .: ([#] (CompactSublatt L))
A4: the carrier of (CompactSublatt Imc) c= the carrier of Imc by YELLOW_0:def_13;
then reconsider a = a9 as Element of Imc by A3;
 a is compact by A3, Def1;
then A5: a << a by WAYBEL_3:def_2;
 a9 in the carrier of Imc by A3, A4;
then  a in rng c by YELLOW_0:def_15;
then consider a1 being Element of L such that
A6: a = a1 and
A7: a1 = c . a1 by A2;
 compactbelow a1 is non empty directed Subset of L by Def4;
then A8: ( c preserves_sup_of compactbelow a1 & ex_sup_of compactbelow a1,L ) by A1, WAYBEL_0:75, WAYBEL_0:def_37;
A9: c is monotone by A1, YELLOW_2:16;
now__::_thesis:_for_z_being_set_st_z_in_c_.:_(compactbelow_a1)_holds_
z_in_(downarrow_a1)_/\_(c_.:_([#]_(CompactSublatt_L)))
let z be set ; ::_thesis: ( z in c .: (compactbelow a1) implies z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) )
assume  z in c .: (compactbelow a1) ; ::_thesis: z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L)))
then consider v being set  such that
A10: v in dom c and
A11: v in compactbelow a1 and
A12: z = c . v by FUNCT_1:def_6;
reconsider v9 = v as Element of L by A11;
A13: v in (downarrow a1) /\ the carrier of (CompactSublatt L) by A11, Th5;
then  v in downarrow a1 by XBOOLE_0:def_4;
then  v9 <= a1 by WAYBEL_0:17;
then  c . v9 <= a1 by A7, A9, WAYBEL_1:def_2;
then A14: z in downarrow a1 by A12, WAYBEL_0:17;
 v in [#] (CompactSublatt L) by A13, XBOOLE_0:def_4;
then  z in c .: ([#] (CompactSublatt L)) by A10, A12, FUNCT_1:def_6;
hence  z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) by A14, XBOOLE_0:def_4; ::_thesis: verum
end;
then A15: c .: (compactbelow a1) c= (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) by TARSKI:def_3;
 a = sup (compactbelow a1) by A6, Def3;
then A16: a = sup (c .: (compactbelow a1)) by A6, A7, A8, WAYBEL_0:def_31;
 c .: (compactbelow a1) c= rng c by RELAT_1:111;
then A17: c .: (compactbelow a1) c= the carrier of Imc by YELLOW_0:def_15;
A18: (downarrow a) /\ (c .: ([#] (CompactSublatt L))) is non empty directed Subset of Imc
proof
 (c .: ([#] (CompactSublatt L))) /\ (downarrow a) is Subset of Imc ;
then reconsider D = (downarrow a) /\ (c .: ([#] (CompactSublatt L))) as Subset of Imc ;
A19: Bottom Imc <= a by YELLOW_0:44;
A20: now__::_thesis:_for_x,_y_being_Element_of_Imc_st_x_in_D_&_y_in_D_holds_
ex_z_being_Element_of_Imc_st_
(_z_in_D_&_x_<=_z_&_y_<=_z_)
let x, y be Element of Imc; ::_thesis: ( x in D & y in D implies ex z being Element of Imc st
( z in D & x <= z & y <= z ) )
assume that
A21: x in D and
A22: y in D ; ::_thesis: ex z being Element of Imc st
( z in D & x <= z & y <= z )
 x in c .: ([#] (CompactSublatt L)) by A21, XBOOLE_0:def_4;
then consider d being set  such that
A23: d in dom c and
A24: d in [#] (CompactSublatt L) and
A25: x = c . d by FUNCT_1:def_6;
 y in c .: ([#] (CompactSublatt L)) by A22, XBOOLE_0:def_4;
then consider e being set  such that
A26: e in dom c and
A27: e in [#] (CompactSublatt L) and
A28: y = c . e by FUNCT_1:def_6;
reconsider e = e as Element of L by A26;
 y in downarrow a by A22, XBOOLE_0:def_4;
then  y <= a by WAYBEL_0:17;
then A29: c . e <= a1 by A6, A28, YELLOW_0:59;
reconsider d = d as Element of L by A23;
A30: d <= d "\/" e by YELLOW_0:22;
 x in downarrow a by A21, XBOOLE_0:def_4;
then  x <= a by WAYBEL_0:17;
then  c . d <= a1 by A6, A25, YELLOW_0:59;
then A31: (c . d) "\/" (c . e) <= a1 by A29, YELLOW_0:22;
 d "\/" e in the carrier of L ;
then  d "\/" e in dom c by FUNCT_2:def_1;
then  c . (d "\/" e) in rng c by FUNCT_1:def_3;
then reconsider z = c . (d "\/" e) as Element of Imc by YELLOW_0:def_15;
take z = z; ::_thesis: ( z in D & x <= z & y <= z )
A32: id L <= c by WAYBEL_1:def_14;
then  (id L) . e <= c . e by YELLOW_2:9;
then A33: e <= c . e by FUNCT_1:18;
 (id L) . d <= c . d by A32, YELLOW_2:9;
then  d <= c . d by FUNCT_1:18;
then  d "\/" e <= (c . d) "\/" (c . e) by A33, YELLOW_3:3;
then  d "\/" e <= a1 by A31, ORDERS_2:3;
then  c . (d "\/" e) <= a1 by A7, A9, WAYBEL_1:def_2;
then  z <= a by A6, YELLOW_0:60;
then A34: z in downarrow a by WAYBEL_0:17;
A35: e <= d "\/" e by YELLOW_0:22;
then A36: c . e <= c . (d "\/" e) by A9, WAYBEL_1:def_2;
 e is compact by A27, Def1;
then  e << e by WAYBEL_3:def_2;
then A37: e << d "\/" e by A35, WAYBEL_3:2;
 d is compact by A24, Def1;
then  d << d by WAYBEL_3:def_2;
then  d << d "\/" e by A30, WAYBEL_3:2;
then  d "\/" e << d "\/" e by A37, WAYBEL_3:3;
then  d "\/" e is compact by WAYBEL_3:def_2;
then A38: d "\/" e in [#] (CompactSublatt L) by Def1;
 d "\/" e in the carrier of L ;
then  d "\/" e in dom c by FUNCT_2:def_1;
then  z in c .: ([#] (CompactSublatt L)) by A38, FUNCT_1:def_6;
hence  z in D by A34, XBOOLE_0:def_4; ::_thesis: ( x <= z & y <= z )
 c . d <= c . (d "\/" e) by A9, A30, WAYBEL_1:def_2;
hence  ( x <= z & y <= z ) by A25, A28, A36, YELLOW_0:60; ::_thesis: verum
end;
 Bottom L is compact by WAYBEL_3:15;
then  ( dom c = the carrier of L & Bottom L in [#] (CompactSublatt L) ) by Def1, FUNCT_2:def_1;
then A39: c . (Bottom L) in c .: ([#] (CompactSublatt L)) by FUNCT_1:def_6;
A40: ( ex_sup_of {} ,L & {} c= the carrier of L ) by XBOOLE_1:2, YELLOW_0:42;
A41: {} c= the carrier of Imc by XBOOLE_1:2;
c . (Bottom L) = c . ("\/" ({},L)) by YELLOW_0:def_11
.= "\/" ({},Imc) by A40, A41, WAYBEL_1:55
.= Bottom Imc by YELLOW_0:def_11 ;
then  c . (Bottom L) in downarrow a by A19, WAYBEL_0:17;
hence  (downarrow a) /\ (c .: ([#] (CompactSublatt L))) is non empty directed Subset of Imc by A39, A20, WAYBEL_0:def_1, XBOOLE_0:def_4; ::_thesis: verum
end;
A42: c .: ([#] (CompactSublatt L)) c= rng c by RELAT_1:111;
now__::_thesis:_for_z_being_set_st_z_in_(downarrow_a1)_/\_(c_.:_([#]_(CompactSublatt_L)))_holds_
z_in_(downarrow_a)_/\_(c_.:_([#]_(CompactSublatt_L)))
let z be set ; ::_thesis: ( z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) implies z in (downarrow a) /\ (c .: ([#] (CompactSublatt L))) )
assume A43: z in (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) ; ::_thesis: z in (downarrow a) /\ (c .: ([#] (CompactSublatt L)))
then reconsider z1 = z as Element of L ;
A44: z in c .: ([#] (CompactSublatt L)) by A43, XBOOLE_0:def_4;
then reconsider z2 = z1 as Element of Imc by A42, YELLOW_0:def_15;
 z in downarrow a1 by A43, XBOOLE_0:def_4;
then  z1 <= a1 by WAYBEL_0:17;
then  z2 <= a by A6, YELLOW_0:60;
then  z in downarrow a by WAYBEL_0:17;
hence  z in (downarrow a) /\ (c .: ([#] (CompactSublatt L))) by A44, XBOOLE_0:def_4; ::_thesis: verum
end;
then A45: (downarrow a1) /\ (c .: ([#] (CompactSublatt L))) c= (downarrow a) /\ (c .: ([#] (CompactSublatt L))) by TARSKI:def_3;
 ex_sup_of c .: (compactbelow a1),L by A8, WAYBEL_0:def_31;
then A46: a = "\/" ((c .: (compactbelow a1)),Imc) by A6, A7, A17, A16, WAYBEL_1:55;
 ( ex_sup_of c .: (compactbelow a1),Imc & ex_sup_of (downarrow a) /\ (c .: ([#] (CompactSublatt L))),Imc ) by YELLOW_0:17;
then  a <= "\/" (((downarrow a) /\ (c .: ([#] (CompactSublatt L)))),Imc) by A46, A15, A45, XBOOLE_1:1, YELLOW_0:34;
then consider k being Element of Imc such that
A47: k in (downarrow a) /\ (c .: ([#] (CompactSublatt L))) and
A48: a <= k by A5, A18, WAYBEL_3:def_1;
 k in downarrow a by A47, XBOOLE_0:def_4;
then A49: k <= a by WAYBEL_0:17;
 k in c .: ([#] (CompactSublatt L)) by A47, XBOOLE_0:def_4;
hence  a9 in c .: ([#] (CompactSublatt L)) by A48, A49, ORDERS_2:2; ::_thesis: verum
end;
then A50: [#] (CompactSublatt (Image c)) c= c .: ([#] (CompactSublatt L)) by TARSKI:def_3;
 c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) by A1, Th23;
hence  c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c)) by A50, XBOOLE_0:def_10; ::_thesis: verum
end;

begin

theorem Th26: :: WAYBEL_8:26
for X, x being set holds
( x is Element of (BoolePoset X) iff x c= X )
proof
let X, x be set ; ::_thesis: ( x is Element of (BoolePoset X) iff x c= X )
 LattPOSet (BooleLatt X) = RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #) by LATTICE3:def_2;
then A1: the carrier of (BoolePoset X) = the carrier of (BooleLatt X) by YELLOW_1:def_2
.= bool X by LATTICE3:def_1 ;
hence  ( x is Element of (BoolePoset X) implies x c= X ) ; ::_thesis: ( x c= X implies x is Element of (BoolePoset X) )
thus  ( x c= X implies x is Element of (BoolePoset X) ) by A1; ::_thesis: verum
end;

theorem Th27: :: WAYBEL_8:27
for X being set
for x, y being Element of (BoolePoset X) holds
( x << y iff for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z )
proof
let X be set ; ::_thesis: for x, y being Element of (BoolePoset X) holds
( x << y iff for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z )
let x, y be Element of (BoolePoset X); ::_thesis: ( x << y iff for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z )
 LattPOSet (BooleLatt X) = RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #) by LATTICE3:def_2;
then A1: the carrier of (BoolePoset X) = the carrier of (BooleLatt X) by YELLOW_1:def_2
.= bool X by LATTICE3:def_1 ;
thus  ( x << y implies for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z ) ::_thesis: ( ( for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z ) implies x << y )
proof
assume A2: x << y ; ::_thesis: for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z
let Y be Subset-Family of X; ::_thesis: ( y c= union Y implies ex Z being finite Subset of Y st x c= union Z )
reconsider Y9 = Y as Subset of (BoolePoset X) by A1;
assume  y c= union Y ; ::_thesis: ex Z being finite Subset of Y st x c= union Z
then  y c= sup Y9 by YELLOW_1:21;
then  y <= sup Y9 by YELLOW_1:2;
then consider Z being finite Subset of (BoolePoset X) such that
A3: Z c= Y and
A4: x <= sup Z by A2, WAYBEL_3:18;
reconsider Z9 = Z as finite Subset of Y by A3;
take  Z9 ; ::_thesis: x c= union Z9
 x c= sup Z by A4, YELLOW_1:2;
hence  x c= union Z9 by YELLOW_1:21; ::_thesis: verum
end;
thus  ( ( for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z ) implies x << y ) ::_thesis: verum
proof
assume A5: for Y being Subset-Family of X st y c= union Y holds
ex Z being finite Subset of Y st x c= union Z ; ::_thesis: x << y
now__::_thesis:_for_Y_being_Subset_of_(BoolePoset_X)_st_y_<=_sup_Y_holds_
ex_Z_being_finite_Subset_of_(BoolePoset_X)_st_
(_Z_c=_Y_&_x_<=_sup_Z_)
let Y be Subset of (BoolePoset X); ::_thesis: ( y <= sup Y implies ex Z being finite Subset of (BoolePoset X) st
( Z c= Y & x <= sup Z ) )
reconsider Y9 = Y as Subset-Family of X by A1;
assume  y <= sup Y ; ::_thesis: ex Z being finite Subset of (BoolePoset X) st
( Z c= Y & x <= sup Z )
then  y c= sup Y by YELLOW_1:2;
then  y c= union Y9 by YELLOW_1:21;
then consider Z9 being finite Subset of Y9 such that
A6: x c= union Z9 by A5;
reconsider Z = Z9 as finite Subset of (BoolePoset X) by XBOOLE_1:1;
take Z = Z; ::_thesis: ( Z c= Y & x <= sup Z )
thus  Z c= Y ; ::_thesis: x <= sup Z
 x c= sup Z by A6, YELLOW_1:21;
hence  x <= sup Z by YELLOW_1:2; ::_thesis: verum
end;
hence  x << y by WAYBEL_3:19; ::_thesis: verum
end;
end;

theorem Th28: :: WAYBEL_8:28
for X being set
for x being Element of (BoolePoset X) holds
( x is finite iff x is compact )
proof
let X be set ; ::_thesis: for x being Element of (BoolePoset X) holds
( x is finite iff x is compact )
let x be Element of (BoolePoset X); ::_thesis: ( x is finite iff x is compact )
percases ( x is empty or not x is empty ) ;
supposeA1: x is empty ; ::_thesis: ( x is finite iff x is compact )
then  x = Bottom (BoolePoset X) by YELLOW_1:18;
hence  ( x is finite iff x is compact ) by A1, WAYBEL_3:15; ::_thesis: verum
end;
supposeA2: not x is empty ; ::_thesis: ( x is finite iff x is compact )
thus  ( x is finite implies x is compact ) ::_thesis: ( x is compact implies x is finite )
proof
assume A3: x is finite ; ::_thesis: x is compact
now__::_thesis:_for_Y_being_Subset-Family_of_X_st_x_c=_union_Y_holds_
ex_Z_being_finite_Subset_of_Y_st_x_c=_union_Z
defpred S1[ set , set ] means $1 in $2;
let Y be Subset-Family of X; ::_thesis: ( x c= union Y implies ex Z being finite Subset of Y st x c= union Z )
assume A4: x c= union Y ; ::_thesis: ex Z being finite Subset of Y st x c= union Z
A5: for e being set st e in x holds
ex u being set st
( u in Y & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in x implies ex u being set st
( u in Y & S1[e,u] ) )
assume  e in x ; ::_thesis: ex u being set st
( u in Y & S1[e,u] )
then  ex u being set st
( e in u & u in Y ) by A4, TARSKI:def_4;
hence  ex u being set st
( u in Y & S1[e,u] ) ; ::_thesis: verum
end;
consider f being Function such that
A6: dom f = x and
A7: rng f c= Y and
A8: for e being set st e in x holds
S1[e,f . e] from FUNCT_1:sch_5(A5);
reconsider Z = rng f as Subset of Y by A7;
reconsider Z = Z as finite Subset of Y by A3, A6, FINSET_1:8;
take Z = Z; ::_thesis: x c= union Z
now__::_thesis:_for_z_being_set_st_z_in_x_holds_
z_in_union_Z
let z be set ; ::_thesis: ( z in x implies z in union Z )
assume  z in x ; ::_thesis: z in union Z
then  ( z in f . z & f . z in Z ) by A6, A8, FUNCT_1:def_3;
hence  z in union Z by TARSKI:def_4; ::_thesis: verum
end;
hence  x c= union Z by TARSKI:def_3; ::_thesis: verum
end;
then  x << x by Th27;
hence  x is compact by WAYBEL_3:def_2; ::_thesis: verum
end;
thus  ( x is compact implies x is finite ) ::_thesis: verum
proof
reconsider x9 = x as non empty set by A2;
set Y =  {  {y} where y is Element of x9 : verum  }  ;
  {  {y} where y is Element of x9 : verum  }  c= bool X
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in  {  {y} where y is Element of x9 : verum  }  or t in bool X )
assume  t in  {  {y} where y is Element of x9 : verum  }  ; ::_thesis: t in bool X
then A9: ex y9 being Element of x9 st t = {y9} ;
now__::_thesis:_for_k_being_set_st_k_in_t_holds_
k_in_X
let k be set ; ::_thesis: ( k in t implies k in X )
assume A10: k in t ; ::_thesis: k in X
 x c= X by Th26;
hence  k in X by A9, A10, TARSKI:def_3; ::_thesis: verum
end;
then  t c= X by TARSKI:def_3;
hence  t in bool X ; ::_thesis: verum
end;
then reconsider Y =  {  {y} where y is Element of x9 : verum  }  as Subset-Family of X ;
now__::_thesis:_for_y_being_set_st_y_in_x_holds_
y_in_union_Y
let y be set ; ::_thesis: ( y in x implies y in union Y )
assume  y in x ; ::_thesis: y in union Y
then A11: {y} in Y ;
 y in {y} by TARSKI:def_1;
hence  y in union Y by A11, TARSKI:def_4; ::_thesis: verum
end;
then A12: x c= union Y by TARSKI:def_3;
assume  x is compact ; ::_thesis: x is finite
then  x << x by WAYBEL_3:def_2;
then consider Z being finite Subset of Y such that
A13: x c= union Z by A12, Th27;
now__::_thesis:_for_k_being_set_st_k_in_Z_holds_
k_is_finite
let k be set ; ::_thesis: ( k in Z implies k is finite )
assume  k in Z ; ::_thesis: k is finite
then  k in Y ;
then  ex y9 being Element of x9 st k = {y9} ;
hence  k is finite ; ::_thesis: verum
end;
then  union Z is finite by FINSET_1:7;
hence  x is finite by A13; ::_thesis: verum
end;
end;
end;
end;

theorem Th29: :: WAYBEL_8:29
for X being set
for x being Element of (BoolePoset X) holds compactbelow x =  {  y where y is finite Subset of x : verum  }
proof
let X be set ; ::_thesis: for x being Element of (BoolePoset X) holds compactbelow x =  {  y where y is finite Subset of x : verum  }
let x be Element of (BoolePoset X); ::_thesis: compactbelow x =  {  y where y is finite Subset of x : verum  }
now__::_thesis:_for_z_being_set_st_z_in__{__y_where_y_is_finite_Subset_of_x_:_verum__}__holds_
z_in_compactbelow_x
let z be set ; ::_thesis: ( z in  {  y where y is finite Subset of x : verum  }  implies z in compactbelow x )
assume  z in  {  y where y is finite Subset of x : verum  }  ; ::_thesis: z in compactbelow x
then consider z9 being finite Subset of x such that
A1: z9 = z ;
 x c= X by Th26;
then  z9 c= X by XBOOLE_1:1;
then reconsider z1 = z9 as Element of (BoolePoset X) by Th26;
 ( z1 is compact & z1 <= x ) by Th28, YELLOW_1:2;
hence  z in compactbelow x by A1; ::_thesis: verum
end;
then A2:  {  y where y is finite Subset of x : verum  }  c= compactbelow x by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_compactbelow_x_holds_
z_in__{__y_where_y_is_finite_Subset_of_x_:_verum__}_
let z be set ; ::_thesis: ( z in compactbelow x implies z in  {  y where y is finite Subset of x : verum  }  )
assume  z in compactbelow x ; ::_thesis: z in  {  y where y is finite Subset of x : verum  }
then consider z9 being Element of (BoolePoset X) such that
A3: z9 = z and
A4: ( x >= z9 & z9 is compact ) ;
 ( z is finite & z9 c= x ) by A3, A4, Th28, YELLOW_1:2;
hence  z in  {  y where y is finite Subset of x : verum  }  by A3; ::_thesis: verum
end;
then  compactbelow x c=  {  y where y is finite Subset of x : verum  }  by TARSKI:def_3;
hence  compactbelow x =  {  y where y is finite Subset of x : verum  }  by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: WAYBEL_8:30
for X being set
for F being Subset of X holds
( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )
proof
let X be set ; ::_thesis: for F being Subset of X holds
( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )
let F be Subset of X; ::_thesis: ( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )
reconsider F9 = F as Element of (BoolePoset X) by Th26;
A1: F c= F ;
thus  ( F in the carrier of (CompactSublatt (BoolePoset X)) implies F is finite ) ::_thesis: ( F is finite implies F in the carrier of (CompactSublatt (BoolePoset X)) )
proof
assume A2: F in the carrier of (CompactSublatt (BoolePoset X)) ; ::_thesis: F is finite
 the carrier of (CompactSublatt (BoolePoset X)) c= the carrier of (BoolePoset X) by YELLOW_0:def_13;
then reconsider F9 = F as Element of (BoolePoset X) by A2;
 ( F9 <= F9 & F9 is compact ) by A2, Def1;
then  F9 in compactbelow F9 ;
then  F9 in  {  y where y is finite Subset of F9 : verum  }  by Th29;
then  ex F1 being finite Subset of F9 st F1 = F9 ;
hence  F is finite ; ::_thesis: verum
end;
assume  F is finite ; ::_thesis: F in the carrier of (CompactSublatt (BoolePoset X))
then  F in  {  y where y is finite Subset of F9 : verum  }  by A1;
then  F9 in compactbelow F9 by Th29;
then  F9 is compact by Th4;
hence  F in the carrier of (CompactSublatt (BoolePoset X)) by Def1; ::_thesis: verum
end;

registration
let X be set ;
let x be Element of (BoolePoset X);
cluster compactbelow x ->  directed lower ;
coherence
 ( compactbelow x is lower & compactbelow x is directed )
proof
now__::_thesis:_for_a,_b_being_set_st_a_c=_b_&_b_in_compactbelow_x_holds_
a_in_compactbelow_x
let a, b be set ; ::_thesis: ( a c= b & b in compactbelow x implies a in compactbelow x )
assume that
A1: a c= b and
A2: b in compactbelow x ; ::_thesis: a in compactbelow x
 b in  {  y where y is finite Subset of x : verum  }  by A2, Th29;
then  ex b1 being finite Subset of x st b = b1 ;
then  a is finite Subset of x by A1, XBOOLE_1:1;
then  a in  {  y where y is finite Subset of x : verum  }  ;
hence  a in compactbelow x by Th29; ::_thesis: verum
end;
hence A3: compactbelow x is lower by WAYBEL_7:6; ::_thesis: compactbelow x is directed
now__::_thesis:_for_a,_b_being_set_st_a_in_compactbelow_x_&_b_in_compactbelow_x_holds_
a_\/_b_in_compactbelow_x
let a, b be set ; ::_thesis: ( a in compactbelow x & b in compactbelow x implies a \/ b in compactbelow x )
assume that
A4: a in compactbelow x and
A5: b in compactbelow x ; ::_thesis: a \/ b in compactbelow x
 b in  {  y where y is finite Subset of x : verum  }  by A5, Th29;
then A6: ex b1 being finite Subset of x st b = b1 ;
 a in  {  y where y is finite Subset of x : verum  }  by A4, Th29;
then  ex a1 being finite Subset of x st a = a1 ;
then  a \/ b is finite Subset of x by A6, XBOOLE_1:8;
then  a \/ b in  {  y where y is finite Subset of x : verum  }  ;
hence  a \/ b in compactbelow x by Th29; ::_thesis: verum
end;
hence  compactbelow x is directed by A3, WAYBEL_7:8; ::_thesis: verum
end;
end;

theorem Th31: :: WAYBEL_8:31
for X being set holds BoolePoset X is algebraic
proof
let X be set ; ::_thesis: BoolePoset X is algebraic
now__::_thesis:_for_x_being_Element_of_(BoolePoset_X)_holds_x_=_sup_(compactbelow_x)
let x be Element of (BoolePoset X); ::_thesis: x = sup (compactbelow x)
A1: now__::_thesis:_for_a_being_Element_of_(BoolePoset_X)_st_a_is_>=_than_compactbelow_x_holds_
x_<=_a
let a be Element of (BoolePoset X); ::_thesis: ( a is_>=_than compactbelow x implies x <= a )
assume A2: a is_>=_than compactbelow x ; ::_thesis: x <= a
now__::_thesis:_for_t_being_set_st_t_in_x_holds_
t_in_a
let t be set ; ::_thesis: ( t in x implies t in a )
assume A3: t in x ; ::_thesis: t in a
A4: x c= X by Th26;
now__::_thesis:_for_k_being_set_st_k_in_{t}_holds_
k_in_X
let k be set ; ::_thesis: ( k in {t} implies k in X )
assume  k in {t} ; ::_thesis: k in X
then  k = t by TARSKI:def_1;
hence  k in X by A3, A4; ::_thesis: verum
end;
then  {t} c= X by TARSKI:def_3;
then reconsider t1 = {t} as Element of (BoolePoset X) by Th26;
 for k being set st k in {t} holds
k in x by A3, TARSKI:def_1;
then  {t} is finite Subset of x by TARSKI:def_3;
then  {t} in  {  y where y is finite Subset of x : verum  }  ;
then  {t} in compactbelow x by Th29;
then  t1 <= a by A2, LATTICE3:def_9;
then  ( t in {t} & {t} c= a ) by TARSKI:def_1, YELLOW_1:2;
hence  t in a ; ::_thesis: verum
end;
then  x c= a by TARSKI:def_3;
hence  x <= a by YELLOW_1:2; ::_thesis: verum
end;
 for b being Element of (BoolePoset X) st b in compactbelow x holds
b <= x by Th4;
then  x is_>=_than compactbelow x by LATTICE3:def_9;
hence  x = sup (compactbelow x) by A1, YELLOW_0:32; ::_thesis: verum
end;
then  ( ( for x being Element of (BoolePoset X) holds
( not compactbelow x is empty & compactbelow x is directed ) ) & BoolePoset X is satisfying_axiom_K ) by Def3;
hence  BoolePoset X is algebraic by Def4; ::_thesis: verum
end;

registration
let X be set ;
cluster BoolePoset X ->  algebraic ;
coherence
 BoolePoset X is algebraic by Th31;
end;