:: WAYBEL15 semantic presentation

begin

theorem Th1: :: WAYBEL15:1
for R being RelStr
for S being full SubRelStr of R
for T being full SubRelStr of S holds T is full SubRelStr of R
proof
let R be RelStr ; ::_thesis: for S being full SubRelStr of R
for T being full SubRelStr of S holds T is full SubRelStr of R
let S be full SubRelStr of R; ::_thesis: for T being full SubRelStr of S holds T is full SubRelStr of R
let T be full SubRelStr of S; ::_thesis: T is full SubRelStr of R
reconsider T1 = T as SubRelStr of R by YELLOW_6:7;
A1: the carrier of T c= the carrier of S by YELLOW_0:def_13;
 the InternalRel of S = the InternalRel of R |_2 the carrier of S by YELLOW_0:def_14;
then  the InternalRel of T = ( the InternalRel of R |_2 the carrier of S) |_2 the carrier of T by YELLOW_0:def_14
.= the InternalRel of R |_2 the carrier of T by A1, WELLORD1:22 ;
then  T1 is full by YELLOW_0:def_14;
hence  T is full SubRelStr of R ; ::_thesis: verum
end;

Lm1:  for X being set
for Y, Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is onto & g is onto holds
g * f is onto
by FUNCT_2:27;

theorem :: WAYBEL15:2
for X being set
for a being Element of (BoolePoset X) holds uparrow a =  {  Y where Y is Subset of X : a c= Y  }
proof
let X be set ; ::_thesis: for a being Element of (BoolePoset X) holds uparrow a =  {  Y where Y is Subset of X : a c= Y  }
let a be Element of (BoolePoset X); ::_thesis: uparrow a =  {  Y where Y is Subset of X : a c= Y  }
A1:  {  Y where Y is Subset of X : a c= Y  }  c= uparrow a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  Y where Y is Subset of X : a c= Y  }  or x in uparrow a )
assume  x in  {  Y where Y is Subset of X : a c= Y  }  ; ::_thesis: x in uparrow a
then consider x9 being Subset of X such that
A2: x9 = x and
A3: a c= x9 ;
reconsider x9 = x9 as Element of (BoolePoset X) by WAYBEL_8:26;
 a <= x9 by A3, YELLOW_1:2;
hence  x in uparrow a by A2, WAYBEL_0:18; ::_thesis: verum
end;
 uparrow a c=  {  Y where Y is Subset of X : a c= Y  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow a or x in  {  Y where Y is Subset of X : a c= Y  }  )
assume A4: x in uparrow a ; ::_thesis: x in  {  Y where Y is Subset of X : a c= Y  }
then reconsider x9 = x as Element of (BoolePoset X) ;
 a <= x9 by A4, WAYBEL_0:18;
then  ( x9 is Subset of X & a c= x ) by WAYBEL_8:26, YELLOW_1:2;
hence  x in  {  Y where Y is Subset of X : a c= Y  }  ; ::_thesis: verum
end;
hence  uparrow a =  {  Y where Y is Subset of X : a c= Y  }  by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: WAYBEL15:3
for L being non empty antisymmetric upper-bounded RelStr
for a being Element of L st Top L <= a holds
a = Top L
proof
let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: for a being Element of L st Top L <= a holds
a = Top L
let a be Element of L; ::_thesis: ( Top L <= a implies a = Top L )
A1: a <= Top L by YELLOW_0:45;
assume  Top L <= a ; ::_thesis: a = Top L
hence  a = Top L by A1, YELLOW_0:def_3; ::_thesis: verum
end;

theorem Th4: :: WAYBEL15:4
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st g is onto & [g,d] is Galois holds
T, Image d are_isomorphic
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S st g is onto & [g,d] is Galois holds
T, Image d are_isomorphic
let g be Function of S,T; ::_thesis: for d being Function of T,S st g is onto & [g,d] is Galois holds
T, Image d are_isomorphic
let d be Function of T,S; ::_thesis: ( g is onto & [g,d] is Galois implies T, Image d are_isomorphic )
assume that
A1: g is onto and
A2: [g,d] is Galois ; ::_thesis: T, Image d are_isomorphic
 d is V13() by A1, A2, WAYBEL_1:24;
then A3: the carrier of (Image d) |` d is one-to-one by FUNCT_1:58;
A4: d is monotone by A2, WAYBEL_1:8;
A5: now__::_thesis:_for_x,_y_being_Element_of_T_holds_
(_(_x_<=_y_implies_(corestr_d)_._x_<=_(corestr_d)_._y_)_&_(_(corestr_d)_._x_<=_(corestr_d)_._y_implies_x_<=_y_)_)
let x, y be Element of T; ::_thesis: ( ( x <= y implies (corestr d) . x <= (corestr d) . y ) & ( (corestr d) . x <= (corestr d) . y implies x <= y ) )
thus  ( x <= y implies (corestr d) . x <= (corestr d) . y ) by A4, WAYBEL_1:def_2; ::_thesis: ( (corestr d) . x <= (corestr d) . y implies x <= y )
thus  ( (corestr d) . x <= (corestr d) . y implies x <= y ) ::_thesis: verum
proof
 for t being Element of T holds d . t is_minimum_of g " {t} by A1, A2, WAYBEL_1:22;
then A6: g * d = id T by WAYBEL_1:23;
assume A7: (corestr d) . x <= (corestr d) . y ; ::_thesis: x <= y
 y in the carrier of T ;
then A8: y in dom d by FUNCT_2:def_1;
A9: g is monotone by A2, WAYBEL_1:8;
 ( d . x = (corestr d) . x & d . y = (corestr d) . y ) by WAYBEL_1:30;
then  d . x <= d . y by A7, YELLOW_0:59;
then A10: g . (d . x) <= g . (d . y) by A9, WAYBEL_1:def_2;
 x in the carrier of T ;
then  x in dom d by FUNCT_2:def_1;
then  (g * d) . x <= g . (d . y) by A10, FUNCT_1:13;
then  (g * d) . x <= (g * d) . y by A8, FUNCT_1:13;
then  (id T) . x <= y by A6, FUNCT_1:18;
hence  x <= y by FUNCT_1:18; ::_thesis: verum
end;
end;
 rng (corestr d) = the carrier of (Image d) by FUNCT_2:def_3;
then  corestr d is isomorphic by A3, A5, WAYBEL_0:66;
hence  T, Image d are_isomorphic by WAYBEL_1:def_8; ::_thesis: verum
end;

theorem Th5: :: WAYBEL15:5
for L1, L2, L3 being non empty Poset
for g1 being Function of L1,L2
for g2 being Function of L2,L3
for d1 being Function of L2,L1
for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois
proof
let L1, L2, L3 be non empty Poset; ::_thesis: for g1 being Function of L1,L2
for g2 being Function of L2,L3
for d1 being Function of L2,L1
for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois
let g1 be Function of L1,L2; ::_thesis: for g2 being Function of L2,L3
for d1 being Function of L2,L1
for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois
let g2 be Function of L2,L3; ::_thesis: for d1 being Function of L2,L1
for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois
let d1 be Function of L2,L1; ::_thesis: for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois
let d2 be Function of L3,L2; ::_thesis: ( [g1,d1] is Galois & [g2,d2] is Galois implies [(g2 * g1),(d1 * d2)] is Galois )
assume that
A1: [g1,d1] is Galois and
A2: [g2,d2] is Galois ; ::_thesis: [(g2 * g1),(d1 * d2)] is Galois
A3: d1 is monotone by A1, WAYBEL_1:8;
A4: g2 is monotone by A2, WAYBEL_1:8;
A5: now__::_thesis:_for_s_being_Element_of_L3
for_t_being_Element_of_L1_holds_
(_(_s_<=_(g2_*_g1)_._t_implies_(d1_*_d2)_._s_<=_t_)_&_(_(d1_*_d2)_._s_<=_t_implies_s_<=_(g2_*_g1)_._t_)_)
let s be Element of L3; ::_thesis: for t being Element of L1 holds
( ( s <= (g2 * g1) . t implies (d1 * d2) . s <= t ) & ( (d1 * d2) . s <= t implies s <= (g2 * g1) . t ) )
let t be Element of L1; ::_thesis: ( ( s <= (g2 * g1) . t implies (d1 * d2) . s <= t ) & ( (d1 * d2) . s <= t implies s <= (g2 * g1) . t ) )
 s in the carrier of L3 ;
then A6: s in dom d2 by FUNCT_2:def_1;
 t in the carrier of L1 ;
then A7: t in dom g1 by FUNCT_2:def_1;
thus  ( s <= (g2 * g1) . t implies (d1 * d2) . s <= t ) ::_thesis: ( (d1 * d2) . s <= t implies s <= (g2 * g1) . t )
proof
assume  s <= (g2 * g1) . t ; ::_thesis: (d1 * d2) . s <= t
then  s <= g2 . (g1 . t) by A7, FUNCT_1:13;
then  d2 . s <= g1 . t by A2, WAYBEL_1:8;
then  d1 . (d2 . s) <= d1 . (g1 . t) by A3, WAYBEL_1:def_2;
then A8: d1 . (d2 . s) <= (d1 * g1) . t by A7, FUNCT_1:13;
 d1 * g1 <= id L1 by A1, WAYBEL_1:18;
then  (d1 * g1) . t <= (id L1) . t by YELLOW_2:9;
then  d1 . (d2 . s) <= (id L1) . t by A8, ORDERS_2:3;
then  d1 . (d2 . s) <= t by FUNCT_1:18;
hence  (d1 * d2) . s <= t by A6, FUNCT_1:13; ::_thesis: verum
end;
thus  ( (d1 * d2) . s <= t implies s <= (g2 * g1) . t ) ::_thesis: verum
proof
assume  (d1 * d2) . s <= t ; ::_thesis: s <= (g2 * g1) . t
then  d1 . (d2 . s) <= t by A6, FUNCT_1:13;
then  d2 . s <= g1 . t by A1, WAYBEL_1:8;
then  g2 . (d2 . s) <= g2 . (g1 . t) by A4, WAYBEL_1:def_2;
then A9: (g2 * d2) . s <= g2 . (g1 . t) by A6, FUNCT_1:13;
 id L3 <= g2 * d2 by A2, WAYBEL_1:18;
then  (id L3) . s <= (g2 * d2) . s by YELLOW_2:9;
then  (id L3) . s <= g2 . (g1 . t) by A9, ORDERS_2:3;
then  s <= g2 . (g1 . t) by FUNCT_1:18;
hence  s <= (g2 * g1) . t by A7, FUNCT_1:13; ::_thesis: verum
end;
end;
 d2 is monotone by A2, WAYBEL_1:8;
then A10: d1 * d2 is monotone by A3, YELLOW_2:12;
 g1 is monotone by A1, WAYBEL_1:8;
then  g2 * g1 is monotone by A4, YELLOW_2:12;
hence  [(g2 * g1),(d1 * d2)] is Galois by A10, A5, WAYBEL_1:8; ::_thesis: verum
end;

theorem Th6: :: WAYBEL15:6
for L1, L2 being non empty Poset
for f being Function of L1,L2
for f1 being Function of L2,L1 st f1 = f " & f is isomorphic holds
( [f,f1] is Galois & [f1,f] is Galois )
proof
let L1, L2 be non empty Poset; ::_thesis: for f being Function of L1,L2
for f1 being Function of L2,L1 st f1 = f " & f is isomorphic holds
( [f,f1] is Galois & [f1,f] is Galois )
let f be Function of L1,L2; ::_thesis: for f1 being Function of L2,L1 st f1 = f " & f is isomorphic holds
( [f,f1] is Galois & [f1,f] is Galois )
let f1 be Function of L2,L1; ::_thesis: ( f1 = f " & f is isomorphic implies ( [f,f1] is Galois & [f1,f] is Galois ) )
assume that
A1: f1 = f " and
A2: f is isomorphic ; ::_thesis: ( [f,f1] is Galois & [f1,f] is Galois )
A3: f1 is isomorphic by A1, A2, WAYBEL_0:68;
now__::_thesis:_for_t_being_Element_of_L2
for_s_being_Element_of_L1_holds_
(_(_t_<=_f_._s_implies_f1_._t_<=_s_)_&_(_f1_._t_<=_s_implies_t_<=_f_._s_)_)
let t be Element of L2; ::_thesis: for s being Element of L1 holds
( ( t <= f . s implies f1 . t <= s ) & ( f1 . t <= s implies t <= f . s ) )
let s be Element of L1; ::_thesis: ( ( t <= f . s implies f1 . t <= s ) & ( f1 . t <= s implies t <= f . s ) )
 s in the carrier of L1 ;
then A4: s in dom f by FUNCT_2:def_1;
A5: f1 * f = id (dom f) by A1, A2, FUNCT_1:39
.= id L1 by FUNCT_2:def_1 ;
thus  ( t <= f . s implies f1 . t <= s ) ::_thesis: ( f1 . t <= s implies t <= f . s )
proof
assume  t <= f . s ; ::_thesis: f1 . t <= s
then  f1 . t <= f1 . (f . s) by A3, WAYBEL_1:def_2;
then  f1 . t <= (f1 * f) . s by A4, FUNCT_1:13;
hence  f1 . t <= s by A5, FUNCT_1:18; ::_thesis: verum
end;
 t in the carrier of L2 ;
then A6: t in dom f1 by FUNCT_2:def_1;
A7: f * f1 = id (rng f) by A1, A2, FUNCT_1:39
.= id L2 by A2, WAYBEL_0:66 ;
thus  ( f1 . t <= s implies t <= f . s ) ::_thesis: verum
proof
assume  f1 . t <= s ; ::_thesis: t <= f . s
then  f . (f1 . t) <= f . s by A2, WAYBEL_1:def_2;
then  (f * f1) . t <= f . s by A6, FUNCT_1:13;
hence  t <= f . s by A7, FUNCT_1:18; ::_thesis: verum
end;
end;
hence  [f,f1] is Galois by A2, A3, WAYBEL_1:8; ::_thesis: [f1,f] is Galois
now__::_thesis:_for_t_being_Element_of_L1
for_s_being_Element_of_L2_holds_
(_(_t_<=_f1_._s_implies_f_._t_<=_s_)_&_(_f_._t_<=_s_implies_t_<=_f1_._s_)_)
let t be Element of L1; ::_thesis: for s being Element of L2 holds
( ( t <= f1 . s implies f . t <= s ) & ( f . t <= s implies t <= f1 . s ) )
let s be Element of L2; ::_thesis: ( ( t <= f1 . s implies f . t <= s ) & ( f . t <= s implies t <= f1 . s ) )
 s in the carrier of L2 ;
then A8: s in dom f1 by FUNCT_2:def_1;
A9: f * f1 = id (rng f) by A1, A2, FUNCT_1:39
.= id L2 by A2, WAYBEL_0:66 ;
thus  ( t <= f1 . s implies f . t <= s ) ::_thesis: ( f . t <= s implies t <= f1 . s )
proof
assume  t <= f1 . s ; ::_thesis: f . t <= s
then  f . t <= f . (f1 . s) by A2, WAYBEL_1:def_2;
then  f . t <= (f * f1) . s by A8, FUNCT_1:13;
hence  f . t <= s by A9, FUNCT_1:18; ::_thesis: verum
end;
 t in the carrier of L1 ;
then A10: t in dom f by FUNCT_2:def_1;
A11: f1 * f = id (dom f) by A1, A2, FUNCT_1:39
.= id L1 by FUNCT_2:def_1 ;
thus  ( f . t <= s implies t <= f1 . s ) ::_thesis: verum
proof
assume  f . t <= s ; ::_thesis: t <= f1 . s
then  f1 . (f . t) <= f1 . s by A3, WAYBEL_1:def_2;
then  (f1 * f) . t <= f1 . s by A10, FUNCT_1:13;
hence  t <= f1 . s by A11, FUNCT_1:18; ::_thesis: verum
end;
end;
hence  [f1,f] is Galois by A2, A3, WAYBEL_1:8; ::_thesis: verum
end;

theorem Th7: :: WAYBEL15:7
for X being set holds BoolePoset X is arithmetic
proof
let X be set ; ::_thesis: BoolePoset X is arithmetic
now__::_thesis:_for_x,_y_being_Element_of_(CompactSublatt_(BoolePoset_X))_holds_ex_inf_of_{x,y},_CompactSublatt_(BoolePoset_X)
let x, y be Element of (CompactSublatt (BoolePoset X)); ::_thesis: ex_inf_of {x,y}, CompactSublatt (BoolePoset X)
reconsider x9 = x, y9 = y as Element of (BoolePoset X) by YELLOW_0:58;
 x9 is compact by WAYBEL_8:def_1;
then  x9 is finite by WAYBEL_8:28;
then  x9 /\ y9 is finite ;
then  x9 "/\" y9 is finite by YELLOW_1:17;
then  x9 "/\" y9 is compact by WAYBEL_8:28;
then reconsider xy = x9 "/\" y9 as Element of (CompactSublatt (BoolePoset X)) by WAYBEL_8:def_1;
A1: now__::_thesis:_for_z_being_Element_of_(CompactSublatt_(BoolePoset_X))_st_z_<=_x_&_z_<=_y_holds_
xy_>=_z
let z be Element of (CompactSublatt (BoolePoset X)); ::_thesis: ( z <= x & z <= y implies xy >= z )
reconsider z9 = z as Element of (BoolePoset X) by YELLOW_0:58;
assume that
A2: z <= x and
A3: z <= y ; ::_thesis: xy >= z
 z9 <= y9 by A3, YELLOW_0:59;
then A4: z9 c= y9 by YELLOW_1:2;
 z9 <= x9 by A2, YELLOW_0:59;
then  z9 c= x9 by YELLOW_1:2;
then  z9 c= x9 /\ y9 by A4, XBOOLE_1:19;
then  z9 c= x9 "/\" y9 by YELLOW_1:17;
then  z9 <= x9 "/\" y9 by YELLOW_1:2;
hence  xy >= z by YELLOW_0:60; ::_thesis: verum
end;
 x9 /\ y9 c= y9 by XBOOLE_1:17;
then  x9 "/\" y9 c= y9 by YELLOW_1:17;
then  x9 "/\" y9 <= y9 by YELLOW_1:2;
then A5: xy <= y by YELLOW_0:60;
 x9 /\ y9 c= x9 by XBOOLE_1:17;
then  x9 "/\" y9 c= x9 by YELLOW_1:17;
then  x9 "/\" y9 <= x9 by YELLOW_1:2;
then  xy <= x by YELLOW_0:60;
hence  ex_inf_of {x,y}, CompactSublatt (BoolePoset X) by A5, A1, YELLOW_0:19; ::_thesis: verum
end;
then  CompactSublatt (BoolePoset X) is with_infima by YELLOW_0:21;
hence  BoolePoset X is arithmetic by WAYBEL_8:19; ::_thesis: verum
end;

registration
let X be set ;
cluster BoolePoset X ->  arithmetic ;
coherence
 BoolePoset X is arithmetic by Th7;
end;

theorem Th8: :: WAYBEL15:8
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 .: (waybelow x) = waybelow (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 .: (waybelow x) = waybelow (f . x)
let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies for x being Element of L1 holds f .: (waybelow x) = waybelow (f . x) )
assume A1: f is isomorphic ; ::_thesis: for x being Element of L1 holds f .: (waybelow x) = waybelow (f . x)
then reconsider g = f " as Function of L2,L1 by WAYBEL_0:67;
let x be Element of L1; ::_thesis: f .: (waybelow x) = waybelow (f . x)
A2: waybelow (f . x) c= f .: (waybelow x)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in waybelow (f . x) or z in f .: (waybelow x) )
assume  z in waybelow (f . x) ; ::_thesis: z in f .: (waybelow x)
then  z in  {  y where y is Element of L2 : y << f . x  }  by WAYBEL_3:def_3;
then consider z1 being Element of L2 such that
A3: z1 = z and
A4: z1 << f . x ;
 g . z1 in the carrier of L1 ;
then A5: g . z1 in dom f by FUNCT_2:def_1;
 z1 in the carrier of L2 ;
then  z1 in dom g by FUNCT_2:def_1;
then  z1 in rng f by A1, FUNCT_1:33;
then A6: z1 = f . (g . z1) by A1, FUNCT_1:35;
then  g . z1 << x by A1, A4, WAYBEL13:27;
then  g . z1 in waybelow x by WAYBEL_3:7;
hence  z in f .: (waybelow x) by A3, A5, A6, FUNCT_1:def_6; ::_thesis: verum
end;
 f .: (waybelow x) c= waybelow (f . x)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in f .: (waybelow x) or z in waybelow (f . x) )
assume  z in f .: (waybelow x) ; ::_thesis: z in waybelow (f . x)
then consider v being set  such that
 v in dom f and
A7: v in waybelow x and
A8: z = f . v by FUNCT_1:def_6;
 v in  {  y where y is Element of L1 : y << x  }  by A7, WAYBEL_3:def_3;
then consider v1 being Element of L1 such that
A9: v1 = v and
A10: v1 << x ;
 f . v1 << f . x by A1, A10, WAYBEL13:27;
hence  z in waybelow (f . x) by A8, A9, WAYBEL_3:7; ::_thesis: verum
end;
hence  f .: (waybelow x) = waybelow (f . x) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th9: :: WAYBEL15:9
for L1, L2 being non empty Poset st L1,L2 are_isomorphic & L1 is continuous holds
L2 is continuous
proof
let L1, L2 be non empty Poset; ::_thesis: ( L1,L2 are_isomorphic & L1 is continuous implies L2 is continuous )
assume that
A1: L1,L2 are_isomorphic and
A2: L1 is continuous ; ::_thesis: L2 is continuous
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: ( L1 is non empty up-complete Poset & L2 is non empty up-complete Poset ) by A1, A2, WAYBEL13:30;
now__::_thesis:_for_y_being_Element_of_L2_holds_y_=_sup_(waybelow_y)
let y be Element of L2; ::_thesis: y = sup (waybelow y)
A5: ex_sup_of waybelow (g . y),L1 by A2, WAYBEL_0:75;
 f is sups-preserving by A3, WAYBEL13:20;
then A6: f preserves_sup_of waybelow (g . y) by WAYBEL_0:def_33;
 y in the carrier of L2 ;
then A7: y in rng f by A3, WAYBEL_0:66;
hence y = f . (g . y) by A3, FUNCT_1:35
.= f . (sup (waybelow (g . y))) by A2, WAYBEL_3:def_5
.= sup (f .: (waybelow (g . y))) by A6, A5, WAYBEL_0:def_31
.= sup (waybelow (f . (g . y))) by A3, A4, Th8
.= sup (waybelow y) by A3, A7, FUNCT_1:35 ;
::_thesis: verum
end;
then A8: L2 is satisfying_axiom_of_approximation by WAYBEL_3:def_5;
A9: g is isomorphic by A3, WAYBEL_0:68;
A10: now__::_thesis:_for_y_being_Element_of_L2_holds_
(_not_waybelow_y_is_empty_&_waybelow_y_is_directed_)
let y be Element of L2; ::_thesis: ( not waybelow y is empty & waybelow y is directed )
 for Y being finite Subset of (waybelow y) ex z being Element of L2 st
( z in waybelow y & z is_>=_than Y )
proof
let Y be finite Subset of (waybelow y); ::_thesis: ex z being Element of L2 st
( z in waybelow y & z is_>=_than Y )
 Y c= the carrier of L2 by XBOOLE_1:1;
then A11: Y c= rng f by A3, WAYBEL_0:66;
now__::_thesis:_for_u_being_set_st_u_in_g_.:_Y_holds_
u_in_waybelow_(g_._y)
let u be set ; ::_thesis: ( u in g .: Y implies u in waybelow (g . y) )
assume  u in g .: Y ; ::_thesis: u in waybelow (g . y)
then consider v being set  such that
 v in dom g and
A12: v in Y and
A13: u = g . v by FUNCT_1:def_6;
 v in waybelow y by A12;
then  v in  {  k where k is Element of L2 : k << y  }  by WAYBEL_3:def_3;
then consider v1 being Element of L2 such that
A14: v1 = v and
A15: v1 << y ;
 g . v1 << g . y by A9, A4, A15, WAYBEL13:27;
hence  u in waybelow (g . y) by A13, A14, WAYBEL_3:7; ::_thesis: verum
end;
then reconsider X = g .: Y as finite Subset of (waybelow (g . y)) by TARSKI:def_3;
consider x being Element of L1 such that
A16: x in waybelow (g . y) and
A17: x is_>=_than X by A2, WAYBEL_0:1;
 y in the carrier of L2 ;
then  y in rng f by A3, WAYBEL_0:66;
then A18: f . (g . y) = y by A3, FUNCT_1:35;
take z = f . x; ::_thesis: ( z in waybelow y & z is_>=_than Y )
 x << g . y by A16, WAYBEL_3:7;
then  z << y by A3, A4, A18, WAYBEL13:27;
hence  z in waybelow y by WAYBEL_3:7; ::_thesis: z is_>=_than Y
f .: X = f .: (f " Y) by A3, FUNCT_1:85
.= Y by A11, FUNCT_1:77 ;
hence  z is_>=_than Y by A3, A17, WAYBEL13:19; ::_thesis: verum
end;
hence  ( not waybelow y is empty & waybelow y is directed ) by WAYBEL_0:1; ::_thesis: verum
end;
 L2 is up-complete by A1, A2, WAYBEL13:30;
hence  L2 is continuous by A8, A10, WAYBEL_3:def_6; ::_thesis: verum
end;

theorem Th10: :: WAYBEL15:10
for L1, L2 being LATTICE st L1,L2 are_isomorphic & L1 is lower-bounded & L1 is arithmetic holds
L2 is arithmetic
proof
let L1, L2 be LATTICE; ::_thesis: ( L1,L2 are_isomorphic & L1 is lower-bounded & L1 is arithmetic implies L2 is arithmetic )
assume that
A1: L1,L2 are_isomorphic and
A2: ( L1 is lower-bounded & L1 is arithmetic ) ; ::_thesis: L2 is arithmetic
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: L2 is up-complete LATTICE by A1, A2, WAYBEL13:30;
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) )
assume that
A6: x2 in the carrier of (CompactSublatt L2) and
A7: y2 in the carrier of (CompactSublatt L2) and
A8: ex_inf_of {x2,y2},L2 ; ::_thesis: inf {x2,y2} in the carrier of (CompactSublatt L2)
 x2 is compact by A6, WAYBEL_8:def_1;
then  g . x2 is compact by A2, A4, A5, WAYBEL13:28;
then A9: g . x2 in the carrier of (CompactSublatt L1) by WAYBEL_8:def_1;
 y2 is compact by A7, WAYBEL_8:def_1;
then  g . y2 is compact by A2, A4, A5, WAYBEL13:28;
then A10: g . y2 in the carrier of (CompactSublatt L1) by WAYBEL_8:def_1;
 x2 in the carrier of L2 ;
then A11: x2 in dom g by FUNCT_2:def_1;
A12: CompactSublatt L1 is meet-inheriting by A2, WAYBEL_8:def_5;
 y2 in the carrier of L2 ;
then A13: y2 in dom g by FUNCT_2:def_1;
 g is infs-preserving by A4, WAYBEL13:20;
then A14: g preserves_inf_of {x2,y2} by WAYBEL_0:def_32;
then  ex_inf_of g .: {x2,y2},L1 by A8, WAYBEL_0:def_30;
then  ex_inf_of {(g . x2),(g . y2)},L1 by A11, A13, FUNCT_1:60;
then  inf {(g . x2),(g . y2)} in the carrier of (CompactSublatt L1) by A9, A10, A12, YELLOW_0:def_16;
then A15: inf {(g . x2),(g . y2)} is compact by WAYBEL_8:def_1;
g . (inf {x2,y2}) = inf (g .: {x2,y2}) by A8, A14, WAYBEL_0:def_30
.= inf {(g . x2),(g . y2)} by A11, A13, FUNCT_1:60 ;
then  inf {x2,y2} is compact by A2, A4, A5, A15, WAYBEL13:28;
hence  inf {x2,y2} in the carrier of (CompactSublatt L2) by WAYBEL_8:def_1; ::_thesis: verum
end;
then A16: CompactSublatt L2 is meet-inheriting by YELLOW_0:def_16;
 L2 is algebraic by A1, A2, WAYBEL13:32;
hence  L2 is arithmetic by A16, WAYBEL_8:def_5; ::_thesis: verum
end;

Lm2:  for L being lower-bounded LATTICE st L is continuous holds
ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving )
proof
let L be lower-bounded LATTICE; ::_thesis: ( L is continuous implies ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) )
assume A1: L is continuous ; ::_thesis: ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving )
reconsider A = InclPoset (Ids L) as lower-bounded arithmetic LATTICE by WAYBEL13:14;
take  A ; ::_thesis: ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving )
reconsider g = SupMap L as Function of A,L ;
take  g ; ::_thesis: ( g is onto & g is infs-preserving & g is directed-sups-preserving )
 the carrier of L c= rng g
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of L or y in rng g )
assume  y in the carrier of L ; ::_thesis: y in rng g
then reconsider y9 = y as Element of L ;
 downarrow y9 is Element of A by YELLOW_2:41;
then  downarrow y9 in the carrier of A ;
then A2: downarrow y9 in dom g by FUNCT_2:def_1;
g . (downarrow y9) = sup (downarrow y9) by YELLOW_2:def_3
.= y9 by WAYBEL_0:34 ;
hence  y in rng g by A2, FUNCT_1:def_3; ::_thesis: verum
end;
then  rng g = the carrier of L by XBOOLE_0:def_10;
hence  g is onto by FUNCT_2:def_3; ::_thesis: ( g is infs-preserving & g is directed-sups-preserving )
thus  g is infs-preserving by A1, WAYBEL13:33; ::_thesis: g is directed-sups-preserving
 g is sups-preserving by A1, WAYBEL13:33;
hence  g is directed-sups-preserving ; ::_thesis: verum
end;

theorem Th11: :: WAYBEL15:11
for L1, L2, L3 being non empty Poset
for f being Function of L1,L2
for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds
g * f is directed-sups-preserving
proof
let L1, L2, L3 be non empty Poset; ::_thesis: for f being Function of L1,L2
for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds
g * f is directed-sups-preserving
let f be Function of L1,L2; ::_thesis: for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds
g * f is directed-sups-preserving
let g be Function of L2,L3; ::_thesis: ( f is directed-sups-preserving & g is directed-sups-preserving implies g * f is directed-sups-preserving )
assume that
A1: f is directed-sups-preserving and
A2: g is directed-sups-preserving ; ::_thesis: g * f is directed-sups-preserving
now__::_thesis:_for_X_being_Subset_of_L1_st_not_X_is_empty_&_X_is_directed_holds_
g_*_f_preserves_sup_of_X
let X be Subset of L1; ::_thesis: ( not X is empty & X is directed implies g * f preserves_sup_of X )
assume A3: ( not X is empty & X is directed ) ; ::_thesis: g * f preserves_sup_of X
 for X1 being Ideal of L1 holds f preserves_sup_of X1 by A1, WAYBEL_0:def_37;
then A4: ( not f .: X is empty & f .: X is directed ) by A3, WAYBEL_0:72, YELLOW_2:15;
now__::_thesis:_(_ex_sup_of_X,L1_implies_(_ex_sup_of_(g_*_f)_.:_X,L3_&_sup_((g_*_f)_.:_X)_=_(g_*_f)_._(sup_X)_)_)
 sup X in the carrier of L1 ;
then A5: sup X in dom f by FUNCT_2:def_1;
assume A6: ex_sup_of X,L1 ; ::_thesis: ( ex_sup_of (g * f) .: X,L3 & sup ((g * f) .: X) = (g * f) . (sup X) )
A7: f preserves_sup_of X by A1, A3, WAYBEL_0:def_37;
then A8: ex_sup_of f .: X,L2 by A6, WAYBEL_0:def_31;
A9: g preserves_sup_of f .: X by A2, A4, WAYBEL_0:def_37;
then A10: sup (g .: (f .: X)) = g . (sup (f .: X)) by A8, WAYBEL_0:def_31;
 ex_sup_of g .: (f .: X),L3 by A8, A9, WAYBEL_0:def_31;
hence  ex_sup_of (g * f) .: X,L3 by RELAT_1:126; ::_thesis: sup ((g * f) .: X) = (g * f) . (sup X)
 sup (f .: X) = f . (sup X) by A6, A7, WAYBEL_0:def_31;
hence  sup ((g * f) .: X) = g . (f . (sup X)) by A10, RELAT_1:126
.= (g * f) . (sup X) by A5, FUNCT_1:13 ;
::_thesis: verum
end;
hence  g * f preserves_sup_of X by WAYBEL_0:def_31; ::_thesis: verum
end;
hence  g * f is directed-sups-preserving by WAYBEL_0:def_37; ::_thesis: verum
end;

begin

theorem :: WAYBEL15:12
for L1, L2 being non empty RelStr
for f being Function of L1,L2
for X being Subset of (Image f) holds (inclusion f) .: X = X by FUNCT_1:92;

theorem Th13: :: WAYBEL15:13
for X being set
for c being Function of (BoolePoset X),(BoolePoset X) st c is idempotent & c is directed-sups-preserving holds
inclusion c is directed-sups-preserving
proof
let X be set ; ::_thesis: for c being Function of (BoolePoset X),(BoolePoset X) st c is idempotent & c is directed-sups-preserving holds
inclusion c is directed-sups-preserving
let c be Function of (BoolePoset X),(BoolePoset X); ::_thesis: ( c is idempotent & c is directed-sups-preserving implies inclusion c is directed-sups-preserving )
assume A1: ( c is idempotent & c is directed-sups-preserving ) ; ::_thesis: inclusion c is directed-sups-preserving
now__::_thesis:_for_Y_being_Ideal_of_(Image_c)_holds_inclusion_c_preserves_sup_of_Y
let Y be Ideal of (Image c); ::_thesis: inclusion c preserves_sup_of Y
now__::_thesis:_(_ex_sup_of_Y,_Image_c_implies_(_ex_sup_of_(inclusion_c)_.:_Y,_BoolePoset_X_&_sup_((inclusion_c)_.:_Y)_=_(inclusion_c)_._(sup_Y)_)_)
 "\/" (Y,(BoolePoset X)) in the carrier of (BoolePoset X) ;
then  "\/" (Y,(BoolePoset X)) in dom c by FUNCT_2:def_1;
then A2: c . ("\/" (Y,(BoolePoset X))) in rng c by FUNCT_1:def_3;
 Y c= the carrier of (Image c) ;
then A3: Y c= rng c by YELLOW_0:def_15;
reconsider Y9 = Y as non empty directed Subset of (BoolePoset X) by YELLOW_2:7;
assume  ex_sup_of Y, Image c ; ::_thesis: ( ex_sup_of (inclusion c) .: Y, BoolePoset X & sup ((inclusion c) .: Y) = (inclusion c) . (sup Y) )
A4: ex_sup_of Y, BoolePoset X by YELLOW_0:17;
 c preserves_sup_of Y9 by A1, WAYBEL_0:def_37;
then  "\/" ((c .: Y),(BoolePoset X)) in rng c by A4, A2, WAYBEL_0:def_31;
then  "\/" (Y,(BoolePoset X)) in rng c by A1, A3, YELLOW_2:20;
then A5: "\/" (Y,(BoolePoset X)) in the carrier of (Image c) by YELLOW_0:def_15;
thus  ex_sup_of (inclusion c) .: Y, BoolePoset X by YELLOW_0:17; ::_thesis: sup ((inclusion c) .: Y) = (inclusion c) . (sup Y)
thus  sup ((inclusion c) .: Y) = "\/" (Y,(BoolePoset X)) by FUNCT_1:92
.= sup Y by A4, A5, YELLOW_0:64
.= (inclusion c) . (sup Y) by FUNCT_1:18 ; ::_thesis: verum
end;
hence  inclusion c preserves_sup_of Y by WAYBEL_0:def_31; ::_thesis: verum
end;
hence  inclusion c is directed-sups-preserving by WAYBEL_0:73; ::_thesis: verum
end;

Lm3:  for L being lower-bounded LATTICE st ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) holds
ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic )
proof
let L be lower-bounded LATTICE; ::_thesis: ( ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) implies ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) )
given A being lower-bounded algebraic LATTICE, g being Function of A,L such that A1: g is onto and
A2: g is infs-preserving and
A3: g is directed-sups-preserving ; ::_thesis: ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic )
 g is upper_adjoint by A2, WAYBEL_1:16;
then consider d being Function of L,A such that
A4: [g,d] is Galois by WAYBEL_1:def_11;
 ( g is monotone & d is monotone ) by A4, WAYBEL_1:8;
then  d * g is monotone by YELLOW_2:12;
then reconsider k = d * g as kernel Function of A,A by A4, WAYBEL_1:41;
 d is lower_adjoint by A4, WAYBEL_1:9;
then A5: k is directed-sups-preserving by A3, Th11;
consider X being non empty set , c being closure Function of (BoolePoset X),(BoolePoset X) such that
A6: c is directed-sups-preserving and
A7: A, Image c are_isomorphic by WAYBEL13:35;
consider f being Function of A,(Image c) such that
A8: f is isomorphic by A7, WAYBEL_1:def_8;
reconsider f1 = f " as Function of (Image c),A by A8, WAYBEL_0:67;
reconsider p = ((((inclusion c) * f) * k) * f1) * (corestr c) as Function of (BoolePoset X),(BoolePoset X) ;
A9: f1 * f = id (dom f) by A8, FUNCT_1:39
.= id A by FUNCT_2:def_1 ;
A10: f1 is isomorphic by A8, WAYBEL_0:68;
then  rng f1 = the carrier of A by WAYBEL_0:66;
then  f1 is onto by FUNCT_2:def_3;
then A11: g * f1 is onto by A1, Lm1;
then  (g * f1) * (corestr c) is onto by Lm1;
then A12: rng ((g * f1) * (corestr c)) = the carrier of L by FUNCT_2:def_3
.= dom (((inclusion c) * f) * d) by FUNCT_2:def_1 ;
A13: f is sups-preserving by A8, WAYBEL13:20;
 inclusion c is directed-sups-preserving by A6, Th13;
then  (inclusion c) * f is directed-sups-preserving by A13, Th11;
then A14: ((inclusion c) * f) * k is directed-sups-preserving by A5, Th11;
take  X ; ::_thesis: ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic )
A15: dom (f * d) = the carrier of L by FUNCT_2:def_1;
A16: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_
(f_*_d)_._x_=_(((inclusion_c)_*_f)_*_d)_._x
let x be set ; ::_thesis: ( x in the carrier of L implies (f * d) . x = (((inclusion c) * f) * d) . x )
assume A17: x in the carrier of L ; ::_thesis: (f * d) . x = (((inclusion c) * f) * d) . x
then  (f * d) . x in the carrier of (Image c) by FUNCT_2:5;
hence (f * d) . x = (inclusion c) . ((f * d) . x) by FUNCT_1:18
.= ((inclusion c) * (f * d)) . x by A15, A17, FUNCT_1:13
.= (((inclusion c) * f) * d) . x by RELAT_1:36 ;
::_thesis: verum
end;
A18: ((((inclusion c) * f) * k) * (f1 * (id (Image c)))) * (f * (k * (f1 * (corestr c)))) = ((((inclusion c) * f) * k) * f1) * (f * (k * (f1 * (corestr c)))) by FUNCT_2:17
.= (((((inclusion c) * f) * k) * f1) * f) * (k * (f1 * (corestr c))) by RELAT_1:36
.= ((((inclusion c) * f) * k) * (id A)) * (k * (f1 * (corestr c))) by A9, RELAT_1:36
.= (((inclusion c) * f) * k) * (k * (f1 * (corestr c))) by FUNCT_2:17
.= ((((inclusion c) * f) * k) * k) * (f1 * (corestr c)) by RELAT_1:36
.= (((inclusion c) * f) * (k * k)) * (f1 * (corestr c)) by RELAT_1:36
.= (((inclusion c) * f) * k) * (f1 * (corestr c)) by QUANTAL1:def_9
.= p by RELAT_1:36 ;
p * p = (((((inclusion c) * f) * k) * f1) * (corestr c)) * ((((inclusion c) * f) * k) * (f1 * (corestr c))) by RELAT_1:36
.= (((((inclusion c) * f) * k) * f1) * (corestr c)) * (((inclusion c) * f) * (k * (f1 * (corestr c)))) by RELAT_1:36
.= (((((inclusion c) * f) * k) * f1) * (corestr c)) * ((inclusion c) * (f * (k * (f1 * (corestr c))))) by RELAT_1:36
.= ((((((inclusion c) * f) * k) * f1) * (corestr c)) * (inclusion c)) * (f * (k * (f1 * (corestr c)))) by RELAT_1:36
.= (((((inclusion c) * f) * k) * f1) * ((corestr c) * (inclusion c))) * (f * (k * (f1 * (corestr c)))) by RELAT_1:36
.= (((((inclusion c) * f) * k) * f1) * (id (Image c))) * (f * (k * (f1 * (corestr c)))) by WAYBEL_1:33
.= p by A18, RELAT_1:36 ;
then A19: p is idempotent by QUANTAL1:def_9;
 (inclusion c) * f is monotone by A8, YELLOW_2:12;
then  ((inclusion c) * f) * k is monotone by YELLOW_2:12;
then  (((inclusion c) * f) * k) * f1 is monotone by A10, YELLOW_2:12;
then  p is monotone by YELLOW_2:12;
then reconsider p = p as projection Function of (BoolePoset X),(BoolePoset X) by A19, WAYBEL_1:def_13;
take  p ; ::_thesis: ( p is directed-sups-preserving & L, Image p are_isomorphic )
p = (((((inclusion c) * f) * d) * g) * f1) * (corestr c) by RELAT_1:36
.= ((((inclusion c) * f) * d) * g) * (f1 * (corestr c)) by RELAT_1:36
.= (((inclusion c) * f) * d) * (g * (f1 * (corestr c))) by RELAT_1:36
.= (((inclusion c) * f) * d) * ((g * f1) * (corestr c)) by RELAT_1:36 ;
then A20: rng (((inclusion c) * f) * d) = rng p by A12, RELAT_1:28;
 dom (((inclusion c) * f) * d) = the carrier of L by FUNCT_2:def_1;
then  rng (f * d) = rng (((inclusion c) * f) * d) by A15, A16, FUNCT_1:2;
then A21: the carrier of (subrelstr (rng (f * d))) = rng (((inclusion c) * f) * d) by YELLOW_0:def_15;
 [f1,f] is Galois by A8, Th6;
then  [(g * f1),(f * d)] is Galois by A4, Th5;
then A22: L, Image (f * d) are_isomorphic by A11, Th4;
 f1 is sups-preserving by A10, WAYBEL13:20;
then  ( corestr c is sups-preserving & (((inclusion c) * f) * k) * f1 is directed-sups-preserving ) by A14, Th11, WAYBEL_1:55;
hence  p is directed-sups-preserving by Th11; ::_thesis: L, Image p are_isomorphic
 subrelstr (rng (f * d)) is strict full SubRelStr of BoolePoset X by Th1;
hence  L, Image p are_isomorphic by A22, A21, A20, YELLOW_0:def_15; ::_thesis: verum
end;

theorem Th14: :: WAYBEL15:14
for L being complete continuous LATTICE
for p being kernel Function of L,L st p is directed-sups-preserving holds
Image p is continuous LATTICE
proof
let L be complete continuous LATTICE; ::_thesis: for p being kernel Function of L,L st p is directed-sups-preserving holds
Image p is continuous LATTICE
let p be kernel Function of L,L; ::_thesis: ( p is directed-sups-preserving implies Image p is continuous LATTICE )
assume A1: p is directed-sups-preserving ; ::_thesis: Image p is continuous LATTICE
now__::_thesis:_for_X_being_Subset_of_L_st_not_X_is_empty_&_X_is_directed_holds_
corestr_p_preserves_sup_of_X
let X be Subset of L; ::_thesis: ( not X is empty & X is directed implies corestr p preserves_sup_of X )
assume  ( not X is empty & X is directed ) ; ::_thesis: corestr p preserves_sup_of X
then A2: p preserves_sup_of X by A1, WAYBEL_0:def_37;
A3: Image p is sups-inheriting by WAYBEL_1:53;
now__::_thesis:_(_ex_sup_of_X,L_implies_(_ex_sup_of_(corestr_p)_.:_X,_Image_p_&_sup_((corestr_p)_.:_X)_=_(corestr_p)_._(sup_X)_)_)
assume A4: ex_sup_of X,L ; ::_thesis: ( ex_sup_of (corestr p) .: X, Image p & sup ((corestr p) .: X) = (corestr p) . (sup X) )
 Image p is complete by WAYBEL_1:54;
hence  ex_sup_of (corestr p) .: X, Image p by YELLOW_0:17; ::_thesis: sup ((corestr p) .: X) = (corestr p) . (sup X)
A5: (corestr p) .: X = p .: X by WAYBEL_1:30;
 ex_sup_of p .: X,L by YELLOW_0:17;
then  "\/" (((corestr p) .: X),L) in the carrier of (Image p) by A3, A5, YELLOW_0:def_19;
hence  sup ((corestr p) .: X) = sup (p .: X) by A5, YELLOW_0:68
.= p . (sup X) by A2, A4, WAYBEL_0:def_31
.= (corestr p) . (sup X) by WAYBEL_1:30 ;
::_thesis: verum
end;
hence  corestr p preserves_sup_of X by WAYBEL_0:def_31; ::_thesis: verum
end;
then  corestr p is directed-sups-preserving by WAYBEL_0:def_37;
hence  Image p is continuous LATTICE by WAYBEL_1:56, WAYBEL_5:33; ::_thesis: verum
end;

theorem Th15: :: WAYBEL15:15
for L being complete continuous LATTICE
for p being projection Function of L,L st p is directed-sups-preserving holds
Image p is continuous LATTICE
proof
let L be complete continuous LATTICE; ::_thesis: for p being projection Function of L,L st p is directed-sups-preserving holds
Image p is continuous LATTICE
let p be projection Function of L,L; ::_thesis: ( p is directed-sups-preserving implies Image p is continuous LATTICE )
assume A1: p is directed-sups-preserving ; ::_thesis: Image p is continuous LATTICE
reconsider Lk =  {  k where k is Element of L : p . k <= k  }  as non empty Subset of L by WAYBEL_1:43;
A2: subrelstr Lk is infs-inheriting by WAYBEL_1:50;
reconsider pk = p | Lk as Function of (subrelstr Lk),(subrelstr Lk) by WAYBEL_1:46;
A3: pk is kernel by WAYBEL_1:48;
now__::_thesis:_for_X_being_Subset_of_(subrelstr_Lk)_st_not_X_is_empty_&_X_is_directed_holds_
pk_preserves_sup_of_X
let X be Subset of (subrelstr Lk); ::_thesis: ( not X is empty & X is directed implies pk preserves_sup_of X )
reconsider X9 = X as Subset of L by WAYBEL13:3;
assume A4: ( not X is empty & X is directed ) ; ::_thesis: pk preserves_sup_of X
then reconsider X9 = X9 as non empty directed Subset of L by YELLOW_2:7;
A5: p preserves_sup_of X9 by A1, WAYBEL_0:def_37;
now__::_thesis:_(_ex_sup_of_X,_subrelstr_Lk_implies_(_ex_sup_of_pk_.:_X,_subrelstr_Lk_&_sup_(pk_.:_X)_=_pk_._(sup_X)_)_)
 X c= the carrier of (subrelstr Lk) ;
then  X c= Lk by YELLOW_0:def_15;
then A6: pk .: X = p .: X by RELAT_1:129;
assume  ex_sup_of X, subrelstr Lk ; ::_thesis: ( ex_sup_of pk .: X, subrelstr Lk & sup (pk .: X) = pk . (sup X) )
 subrelstr Lk is infs-inheriting by WAYBEL_1:50;
then  subrelstr Lk is complete LATTICE by YELLOW_2:30;
hence  ex_sup_of pk .: X, subrelstr Lk by YELLOW_0:17; ::_thesis: sup (pk .: X) = pk . (sup X)
A7: ex_sup_of X,L by YELLOW_0:17;
A8: subrelstr Lk is directed-sups-inheriting by A1, WAYBEL_1:52;
then A9: ( dom pk = the carrier of (subrelstr Lk) & sup X9 = sup X ) by A4, A7, FUNCT_2:def_1, WAYBEL_0:7;
 ( ex_sup_of p .: X,L & pk .: X is directed Subset of (subrelstr Lk) ) by A3, A4, YELLOW_0:17, YELLOW_2:15;
hence  sup (pk .: X) = sup (p .: X) by A4, A8, A6, WAYBEL_0:7
.= p . (sup X9) by A5, A7, WAYBEL_0:def_31
.= pk . (sup X) by A9, FUNCT_1:47 ;
::_thesis: verum
end;
hence  pk preserves_sup_of X by WAYBEL_0:def_31; ::_thesis: verum
end;
then A10: pk is directed-sups-preserving by WAYBEL_0:def_37;
 subrelstr Lk is directed-sups-inheriting by A1, WAYBEL_1:52;
then A11: subrelstr Lk is continuous LATTICE by A2, WAYBEL_5:28;
A12: the carrier of (subrelstr (rng p)) = rng p by YELLOW_0:def_15
.= rng pk by WAYBEL_1:44
.= the carrier of (subrelstr (rng pk)) by YELLOW_0:def_15 ;
 subrelstr (rng pk) is full SubRelStr of L by Th1;
then A13: Image p = Image pk by A12, YELLOW_0:57;
 subrelstr Lk is complete by A2, YELLOW_2:30;
hence  Image p is continuous LATTICE by A11, A3, A13, A10, Th14; ::_thesis: verum
end;

Lm4:  for L being LATTICE st ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) holds
L is continuous
proof
let L be LATTICE; ::_thesis: ( ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous )
given X being set , p being projection Function of (BoolePoset X),(BoolePoset X) such that A1: p is directed-sups-preserving and
A2: L, Image p are_isomorphic ; ::_thesis: L is continuous
 Image p is continuous by A1, Th15;
hence  L is continuous by A2, Th9, WAYBEL_1:6; ::_thesis: verum
end;

theorem :: WAYBEL15:16
for L being lower-bounded LATTICE holds
( L is continuous iff ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) )
proof
let L be lower-bounded LATTICE; ::_thesis: ( L is continuous iff ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) )
thus  ( L is continuous implies ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) ) by Lm2; ::_thesis: ( ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) implies L is continuous )
thus  ( ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) implies L is continuous ) ::_thesis: verum
proof
assume  ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) ; ::_thesis: L is continuous
then  ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) by Lm3;
hence  L is continuous by Lm4; ::_thesis: verum
end;
end;

theorem :: WAYBEL15:17
for L being lower-bounded LATTICE holds
( L is continuous iff ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) )
proof
let L be lower-bounded LATTICE; ::_thesis: ( L is continuous iff ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) )
thus  ( L is continuous implies ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) ) ::_thesis: ( ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) implies L is continuous )
proof
assume  L is continuous ; ::_thesis: ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving )
then  ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) by Lm2;
hence  ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) ; ::_thesis: verum
end;
thus  ( ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) implies L is continuous ) ::_thesis: verum
proof
assume  ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) ; ::_thesis: L is continuous
then  ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) by Lm3;
hence  L is continuous by Lm4; ::_thesis: verum
end;
end;

theorem :: WAYBEL15:18
for L being lower-bounded LATTICE holds
( ( L is continuous implies ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) ) & ( ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous ) )
proof
let L be lower-bounded LATTICE; ::_thesis: ( ( L is continuous implies ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) ) & ( ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous ) )
thus  ( L is continuous implies ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) ) ::_thesis: ( ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous )
proof
assume  L is continuous ; ::_thesis: ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic )
then  ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) by Lm2;
hence  ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) by Lm3; ::_thesis: verum
end;
thus  ( ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous ) by Lm4; ::_thesis: verum
end;

begin

theorem :: WAYBEL15:19
for L being non empty RelStr
for x being Element of L holds
( x in PRIME (L opp) iff x is co-prime )
proof
let L be non empty RelStr ; ::_thesis: for x being Element of L holds
( x in PRIME (L opp) iff x is co-prime )
let x be Element of L; ::_thesis: ( x in PRIME (L opp) iff x is co-prime )
hereby  ::_thesis: ( x is co-prime implies x in PRIME (L opp) )
assume  x in PRIME (L opp) ; ::_thesis: x is co-prime
then  x ~ in PRIME (L opp) by LATTICE3:def_6;
then  x ~ is prime by WAYBEL_6:def_7;
hence  x is co-prime by WAYBEL_6:def_8; ::_thesis: verum
end;
assume  x is co-prime ; ::_thesis: x in PRIME (L opp)
then  x ~ is prime by WAYBEL_6:def_8;
then  x ~ in PRIME (L opp) by WAYBEL_6:def_7;
hence  x in PRIME (L opp) by LATTICE3:def_6; ::_thesis: verum
end;

definition
let L be non empty RelStr ;
let a be Element of L;
attra is atom  means :Def1: :: WAYBEL15:def 1
( Bottom L < a & ( for b being Element of L st Bottom L < b & b <= a holds
b = a ) );
end;

:: deftheorem Def1 defines atom WAYBEL15:def_1_:_
 for L being non empty RelStr
for a being Element of L holds
( a is atom iff ( Bottom L < a & ( for b being Element of L st Bottom L < b & b <= a holds
b = a ) ) );

definition
let L be non empty RelStr ;
func ATOM L ->  Subset of L means :Def2: :: WAYBEL15:def 2
 for x being Element of L holds
( x in it iff x is atom );
existence
 ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff x is atom )
proof
defpred S1[ Element of L] means $1 is atom ;
consider X being Subset of L such that
A1: for x being Element of L holds
( x in X iff S1[x] ) from SUBSET_1:sch_3();
take  X ; ::_thesis: for x being Element of L holds
( x in X iff x is atom )
thus  for x being Element of L holds
( x in X iff x is atom ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is atom ) ) & ( for x being Element of L holds
( x in b2 iff x is atom ) ) holds
b1 = b2
proof
let A1, A2 be Subset of L; ::_thesis: ( ( for x being Element of L holds
( x in A1 iff x is atom ) ) & ( for x being Element of L holds
( x in A2 iff x is atom ) ) implies A1 = A2 )
assume that
A2: for x being Element of L holds
( x in A1 iff x is atom ) and
A3: for x being Element of L holds
( x in A2 iff x is atom ) ; ::_thesis: A1 = A2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_A1_implies_x_in_A2_)_&_(_x_in_A2_implies_x_in_A1_)_)
let x be set ; ::_thesis: ( ( x in A1 implies x in A2 ) & ( x in A2 implies x in A1 ) )
thus  ( x in A1 implies x in A2 ) ::_thesis: ( x in A2 implies x in A1 )
proof
assume A4: x in A1 ; ::_thesis: x in A2
then reconsider x9 = x as Element of L ;
 x9 is atom by A2, A4;
hence  x in A2 by A3; ::_thesis: verum
end;
thus  ( x in A2 implies x in A1 ) ::_thesis: verum
proof
assume A5: x in A2 ; ::_thesis: x in A1
then reconsider x9 = x as Element of L ;
 x9 is atom by A3, A5;
hence  x in A1 by A2; ::_thesis: verum
end;
end;
hence  A1 = A2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines ATOM WAYBEL15:def_2_:_
 for L being non empty RelStr
for b2 being Subset of L holds
( b2 = ATOM L iff for x being Element of L holds
( x in b2 iff x is atom ) );

theorem Th20: :: WAYBEL15:20
for L being Boolean LATTICE
for a being Element of L holds
( a is atom iff ( a is co-prime & a <> Bottom L ) )
proof
let L be Boolean LATTICE; ::_thesis: for a being Element of L holds
( a is atom iff ( a is co-prime & a <> Bottom L ) )
let a be Element of L; ::_thesis: ( a is atom iff ( a is co-prime & a <> Bottom L ) )
thus  ( a is atom implies ( a is co-prime & a <> Bottom L ) ) ::_thesis: ( a is co-prime & a <> Bottom L implies a is atom )
proof
assume A1: a is atom ; ::_thesis: ( a is co-prime & a <> Bottom L )
now__::_thesis:_for_x,_y_being_Element_of_L_st_a_<=_x_"\/"_y_&_not_a_<=_x_holds_
a_<=_y
let x, y be Element of L; ::_thesis: ( a <= x "\/" y & not a <= x implies a <= y )
assume that
A2: a <= x "\/" y and
A3: not a <= x ; ::_thesis: a <= y
A4: a "/\" x <= a by YELLOW_0:23;
 a "/\" x <> a by A3, YELLOW_0:25;
then  not Bottom L < a "/\" x by A1, A4, Def1;
then A5: ( not Bottom L <= a "/\" x or not Bottom L <> a "/\" x ) by ORDERS_2:def_6;
a = a "/\" (x "\/" y) by A2, YELLOW_0:25
.= (a "/\" x) "\/" (a "/\" y) by WAYBEL_1:def_3
.= a "/\" y by A5, WAYBEL_1:3, YELLOW_0:44 ;
hence  a <= y by YELLOW_0:25; ::_thesis: verum
end;
hence  a is co-prime by WAYBEL14:14; ::_thesis: a <> Bottom L
thus  a <> Bottom L by A1, Def1; ::_thesis: verum
end;
assume that
A6: a is co-prime and
A7: a <> Bottom L ; ::_thesis: a is atom
A8: now__::_thesis:_for_b_being_Element_of_L_st_Bottom_L_<_b_&_b_<=_a_holds_
b_=_a
let b be Element of L; ::_thesis: ( Bottom L < b & b <= a implies b = a )
assume that
A9: Bottom L < b and
A10: b <= a ; ::_thesis: b = a
consider c being Element of L such that
A11: c is_a_complement_of b by WAYBEL_1:def_24;
A12: b "/\" c = Bottom L by A11, WAYBEL_1:def_23;
A13: not a <= c
proof
assume  a <= c ; ::_thesis: contradiction
then  b <= c by A10, ORDERS_2:3;
hence  contradiction by A9, A12, YELLOW_0:25; ::_thesis: verum
end;
 b "\/" c = Top L by A11, WAYBEL_1:def_23;
then  a <= b "\/" c by YELLOW_0:45;
then  a <= b by A6, A13, WAYBEL14:14;
hence  b = a by A10, ORDERS_2:2; ::_thesis: verum
end;
 Bottom L <= a by YELLOW_0:44;
then  Bottom L < a by A7, ORDERS_2:def_6;
hence  a is atom by A8, Def1; ::_thesis: verum
end;

registration
let L be Boolean LATTICE;
cluster atom  ->  co-prime for Element of the carrier of L;
coherence
 for b1 being Element of L st b1 is atom holds
b1 is co-prime by Th20;
end;

theorem :: WAYBEL15:21
for L being Boolean LATTICE holds ATOM L = (PRIME (L opp)) \ {(Bottom L)}
proof
let L be Boolean LATTICE; ::_thesis: ATOM L = (PRIME (L opp)) \ {(Bottom L)}
A1: (PRIME (L opp)) \ {(Bottom L)} c= ATOM L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PRIME (L opp)) \ {(Bottom L)} or x in ATOM L )
assume A2: x in (PRIME (L opp)) \ {(Bottom L)} ; ::_thesis: x in ATOM L
then reconsider x9 = x as Element of (L opp) ;
 x in PRIME (L opp) by A2, XBOOLE_0:def_5;
then A3: x9 is prime by WAYBEL_6:def_7;
 not x in {(Bottom L)} by A2, XBOOLE_0:def_5;
then  x9 <> Bottom L by TARSKI:def_1;
then A4: ~ x9 <> Bottom L by LATTICE3:def_7;
(~ x9) ~ = ~ x9 by LATTICE3:def_6
.= x9 by LATTICE3:def_7 ;
then  ~ x9 is co-prime by A3, WAYBEL_6:def_8;
then  ~ x9 is atom by A4, Th20;
then  ~ x9 in ATOM L by Def2;
hence  x in ATOM L by LATTICE3:def_7; ::_thesis: verum
end;
 ATOM L c= (PRIME (L opp)) \ {(Bottom L)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ATOM L or x in (PRIME (L opp)) \ {(Bottom L)} )
assume A5: x in ATOM L ; ::_thesis: x in (PRIME (L opp)) \ {(Bottom L)}
then reconsider x9 = x as Element of L ;
A6: x9 is atom by A5, Def2;
then  x9 ~ is prime by WAYBEL_6:def_8;
then  x9 ~ in PRIME (L opp) by WAYBEL_6:def_7;
then A7: x in PRIME (L opp) by LATTICE3:def_6;
 x <> Bottom L by A6, Th20;
then  not x in {(Bottom L)} by TARSKI:def_1;
hence  x in (PRIME (L opp)) \ {(Bottom L)} by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  ATOM L = (PRIME (L opp)) \ {(Bottom L)} by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: WAYBEL15:22
for L being Boolean LATTICE
for x, a being Element of L st a is atom holds
( a <= x iff not a <= 'not' x )
proof
let L be Boolean LATTICE; ::_thesis: for x, a being Element of L st a is atom holds
( a <= x iff not a <= 'not' x )
let x, a be Element of L; ::_thesis: ( a is atom implies ( a <= x iff not a <= 'not' x ) )
assume A1: a is atom ; ::_thesis: ( a <= x iff not a <= 'not' x )
thus  ( a <= x implies not a <= 'not' x ) ::_thesis: ( not a <= 'not' x implies a <= x )
proof
assume that
A2: a <= x and
A3: a <= 'not' x ; ::_thesis: contradiction
a = a "\/" (Bottom L) by WAYBEL_1:3
.= a "\/" (x "/\" ('not' x)) by YELLOW_5:34
.= (a "\/" x) "/\" (('not' x) "\/" a) by WAYBEL_1:5
.= x "/\" (('not' x) "\/" a) by A2, YELLOW_0:24
.= x "/\" ('not' x) by A3, YELLOW_0:24
.= Bottom L by YELLOW_5:34 ;
hence  contradiction by A1, Th20; ::_thesis: verum
end;
thus  ( not a <= 'not' x implies a <= x ) ::_thesis: verum
proof
 a <= Top L by YELLOW_0:45;
then A4: a <= x "\/" ('not' x) by YELLOW_5:34;
assume  ( not a <= 'not' x & not a <= x ) ; ::_thesis: contradiction
hence  contradiction by A1, A4, WAYBEL14:14; ::_thesis: verum
end;
end;

theorem Th23: :: WAYBEL15:23
for L being complete Boolean LATTICE
for X being Subset of L
for x being Element of L holds x "/\" (sup X) = "\/" ( {  (x "/\" y) where y is Element of L : y in X  }  ,L)
proof
let L be complete Boolean LATTICE; ::_thesis: for X being Subset of L
for x being Element of L holds x "/\" (sup X) = "\/" ( {  (x "/\" y) where y is Element of L : y in X  }  ,L)
let X be Subset of L; ::_thesis: for x being Element of L holds x "/\" (sup X) = "\/" ( {  (x "/\" y) where y is Element of L : y in X  }  ,L)
let x be Element of L; ::_thesis: x "/\" (sup X) = "\/" ( {  (x "/\" y) where y is Element of L : y in X  }  ,L)
 for y being Element of L holds y "/\" is lower_adjoint by WAYBEL_1:def_19;
hence  x "/\" (sup X) = "\/" ( {  (x "/\" y) where y is Element of L : y in X  }  ,L) by WAYBEL_1:64; ::_thesis: verum
end;

theorem Th24: :: WAYBEL15:24
for L being non empty antisymmetric with_infima lower-bounded RelStr
for x, y being Element of L st x is atom & y is atom & x <> y holds
x "/\" y = Bottom L
proof
let L be non empty antisymmetric with_infima lower-bounded RelStr ; ::_thesis: for x, y being Element of L st x is atom & y is atom & x <> y holds
x "/\" y = Bottom L
let x, y be Element of L; ::_thesis: ( x is atom & y is atom & x <> y implies x "/\" y = Bottom L )
assume that
A1: x is atom and
A2: y is atom and
A3: x <> y and
A4: x "/\" y <> Bottom L ; ::_thesis: contradiction
 Bottom L <= x "/\" y by YELLOW_0:44;
then A5: Bottom L < x "/\" y by A4, ORDERS_2:def_6;
A6: x "/\" y <= y by YELLOW_0:23;
 x "/\" y <= x by YELLOW_0:23;
then x = x "/\" y by A1, A5, Def1
.= y by A2, A5, A6, Def1 ;
hence  contradiction by A3; ::_thesis: verum
end;

theorem Th25: :: WAYBEL15:25
for L being complete Boolean LATTICE
for x being Element of L
for A being Subset of L st A c= ATOM L holds
( x in A iff ( x is atom & x <= sup A ) )
proof
let L be complete Boolean LATTICE; ::_thesis: for x being Element of L
for A being Subset of L st A c= ATOM L holds
( x in A iff ( x is atom & x <= sup A ) )
let x be Element of L; ::_thesis: for A being Subset of L st A c= ATOM L holds
( x in A iff ( x is atom & x <= sup A ) )
let A be Subset of L; ::_thesis: ( A c= ATOM L implies ( x in A iff ( x is atom & x <= sup A ) ) )
assume A1: A c= ATOM L ; ::_thesis: ( x in A iff ( x is atom & x <= sup A ) )
thus  ( x in A implies ( x is atom & x <= sup A ) ) ::_thesis: ( x is atom & x <= sup A implies x in A )
proof
assume A2: x in A ; ::_thesis: ( x is atom & x <= sup A )
hence  x is atom by A1, Def2; ::_thesis: x <= sup A
 sup A is_>=_than A by YELLOW_0:32;
hence  x <= sup A by A2, LATTICE3:def_9; ::_thesis: verum
end;
thus  ( x is atom & x <= sup A implies x in A ) ::_thesis: verum
proof
assume that
A3: x is atom and
A4: x <= sup A and
A5: not x in A ; ::_thesis: contradiction
now__::_thesis:_for_b_being_Element_of_L_st_b_in__{__(x_"/\"_y)_where_y_is_Element_of_L_:_y_in_A__}__holds_
b_<=_Bottom_L
let b be Element of L; ::_thesis: ( b in  {  (x "/\" y) where y is Element of L : y in A  }  implies b <= Bottom L )
assume  b in  {  (x "/\" y) where y is Element of L : y in A  }  ; ::_thesis: b <= Bottom L
then consider y being Element of L such that
A6: b = x "/\" y and
A7: y in A ;
 y is atom by A1, A7, Def2;
hence  b <= Bottom L by A3, A5, A6, A7, Th24; ::_thesis: verum
end;
then A8: Bottom L is_>=_than  {  (x "/\" y) where y is Element of L : y in A  }  by LATTICE3:def_9;
x = x "/\" (sup A) by A4, YELLOW_0:25
.= "\/" ( {  (x "/\" y) where y is Element of L : y in A  }  ,L) by Th23 ;
then  x <= Bottom L by A8, YELLOW_0:32;
then  x = Bottom L by YELLOW_5:19;
hence  contradiction by A3, Th20; ::_thesis: verum
end;
end;

theorem Th26: :: WAYBEL15:26
for L being complete Boolean LATTICE
for X, Y being Subset of L st X c= ATOM L & Y c= ATOM L holds
( X c= Y iff sup X <= sup Y )
proof
let L be complete Boolean LATTICE; ::_thesis: for X, Y being Subset of L st X c= ATOM L & Y c= ATOM L holds
( X c= Y iff sup X <= sup Y )
let X, Y be Subset of L; ::_thesis: ( X c= ATOM L & Y c= ATOM L implies ( X c= Y iff sup X <= sup Y ) )
assume that
A1: X c= ATOM L and
A2: Y c= ATOM L ; ::_thesis: ( X c= Y iff sup X <= sup Y )
thus  ( X c= Y implies sup X <= sup Y ) ::_thesis: ( sup X <= sup Y implies X c= Y )
proof
A3: ( ex_sup_of X,L & ex_sup_of Y,L ) by YELLOW_0:17;
assume  X c= Y ; ::_thesis: sup X <= sup Y
hence  sup X <= sup Y by A3, YELLOW_0:34; ::_thesis: verum
end;
thus  ( sup X <= sup Y implies X c= Y ) ::_thesis: verum
proof
assume A4: sup X <= sup Y ; ::_thesis: X c= Y
thus  X c= Y ::_thesis: verum
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X or z in Y )
assume A5: z in X ; ::_thesis: z in Y
then reconsider z1 = z as Element of L ;
 sup X is_>=_than X by YELLOW_0:32;
then  z1 <= sup X by A5, LATTICE3:def_9;
then A6: z1 <= sup Y by A4, ORDERS_2:3;
 z1 is atom by A1, A5, Def2;
hence  z in Y by A2, A6, Th25; ::_thesis: verum
end;
end;
end;

Lm5:  for L being Boolean LATTICE st L is completely-distributive holds
( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) )
proof
let L be Boolean LATTICE; ::_thesis: ( L is completely-distributive implies ( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) ) )
assume A1: L is completely-distributive ; ::_thesis: ( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) )
hence  L is complete ; ::_thesis: for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X )
let x be Element of L; ::_thesis: ex X being Subset of L st
( X c= ATOM L & x = sup X )
consider X1 being Subset of L such that
A2: x = sup X1 and
A3: for y being Element of L st y in X1 holds
y is co-prime by A1, WAYBEL_6:38;
reconsider X = X1 \ {(Bottom L)} as Subset of L ;
A4: now__::_thesis:_for_b_being_Element_of_L_st_b_is_>=_than_X_holds_
x_<=_b
let b be Element of L; ::_thesis: ( b is_>=_than X implies x <= b )
assume A5: b is_>=_than X ; ::_thesis: x <= b
now__::_thesis:_for_c_being_Element_of_L_st_c_in_X1_holds_
c_<=_b
let c be Element of L; ::_thesis: ( c in X1 implies c <= b )
assume A6: c in X1 ; ::_thesis: c <= b
now__::_thesis:_c_<=_b
percases ( c <> Bottom L or c = Bottom L ) ;
suppose c <> Bottom L ; ::_thesis: c <= b
then  not c in {(Bottom L)} by TARSKI:def_1;
then  c in X by A6, XBOOLE_0:def_5;
hence  c <= b by A5, LATTICE3:def_9; ::_thesis: verum
end;
suppose c = Bottom L ; ::_thesis: c <= b
hence  c <= b by YELLOW_0:44; ::_thesis: verum
end;
end;
end;
hence  c <= b ; ::_thesis: verum
end;
then  b is_>=_than X1 by LATTICE3:def_9;
hence  x <= b by A1, A2, YELLOW_0:32; ::_thesis: verum
end;
take  X ; ::_thesis: ( X c= ATOM L & x = sup X )
thus  X c= ATOM L ::_thesis: x = sup X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X or z in ATOM L )
assume A7: z in X ; ::_thesis: z in ATOM L
then reconsider z9 = z as Element of L ;
 not z in {(Bottom L)} by A7, XBOOLE_0:def_5;
then A8: z9 <> Bottom L by TARSKI:def_1;
 z in X1 by A7, XBOOLE_0:def_5;
then  z9 is co-prime by A3;
then  z9 is atom by A8, Th20;
hence  z in ATOM L by Def2; ::_thesis: verum
end;
A9: x is_>=_than X1 by A1, A2, YELLOW_0:32;
now__::_thesis:_for_c_being_Element_of_L_st_c_in_X_holds_
c_<=_x
let c be Element of L; ::_thesis: ( c in X implies c <= x )
assume  c in X ; ::_thesis: c <= x
then  c in X1 by XBOOLE_0:def_5;
hence  c <= x by A9, LATTICE3:def_9; ::_thesis: verum
end;
then  x is_>=_than X by LATTICE3:def_9;
hence  x = sup X by A1, A4, YELLOW_0:32; ::_thesis: verum
end;

Lm6:  for L being Boolean LATTICE st L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) holds
ex Y being set st L, BoolePoset Y are_isomorphic
proof
let L be Boolean LATTICE; ::_thesis: ( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) implies ex Y being set st L, BoolePoset Y are_isomorphic )
assume that
A1: L is complete and
A2: for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ; ::_thesis: ex Y being set st L, BoolePoset Y are_isomorphic
defpred S1[ set , set ] means  ex x9 being Subset of L st
( x9 = $1 & $2 = sup x9 );
take Y = ATOM L; ::_thesis: L, BoolePoset Y are_isomorphic
A3: for x being Element of (BoolePoset Y) ex y being Element of L st S1[x,y]
proof
let x be Element of (BoolePoset Y); ::_thesis: ex y being Element of L st S1[x,y]
 x c= Y by WAYBEL_8:26;
then reconsider x9 = x as Subset of L by XBOOLE_1:1;
take  sup x9 ; ::_thesis: S1[x, sup x9]
take  x9 ; ::_thesis: ( x9 = x & sup x9 = sup x9 )
thus  ( x9 = x & sup x9 = sup x9 ) ; ::_thesis: verum
end;
consider f being Function of (BoolePoset Y),L such that
A4: for x being Element of (BoolePoset Y) holds S1[x,f . x] from FUNCT_2:sch_3(A3);
A5: now__::_thesis:_for_z,_v_being_Element_of_(BoolePoset_Y)_holds_
(_(_z_<=_v_implies_f_._z_<=_f_._v_)_&_(_f_._z_<=_f_._v_implies_z_<=_v_)_)
let z, v be Element of (BoolePoset Y); ::_thesis: ( ( z <= v implies f . z <= f . v ) & ( f . z <= f . v implies z <= v ) )
consider z9 being Subset of L such that
A6: z9 = z and
A7: f . z = sup z9 by A4;
consider v9 being Subset of L such that
A8: v9 = v and
A9: f . v = sup v9 by A4;
A10: ( ex_sup_of z9,L & ex_sup_of v9,L ) by A1, YELLOW_0:17;
thus  ( z <= v implies f . z <= f . v ) ::_thesis: ( f . z <= f . v implies z <= v )
proof
assume  z <= v ; ::_thesis: f . z <= f . v
then  z c= v by YELLOW_1:2;
hence  f . z <= f . v by A6, A7, A8, A9, A10, YELLOW_0:34; ::_thesis: verum
end;
A11: v9 c= ATOM L by A8, WAYBEL_8:26;
A12: z9 c= ATOM L by A6, WAYBEL_8:26;
thus  ( f . z <= f . v implies z <= v ) ::_thesis: verum
proof
assume  f . z <= f . v ; ::_thesis: z <= v
then  z c= v by A1, A6, A7, A8, A9, A12, A11, Th26;
hence  z <= v by YELLOW_1:2; ::_thesis: verum
end;
end;
 the carrier of L c= rng f
proof
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in the carrier of L or k in rng f )
assume  k in the carrier of L ; ::_thesis: k in rng f
then consider K being Subset of L such that
A13: K c= ATOM L and
A14: k = sup K by A2;
A15: K is Element of (BoolePoset Y) by A13, WAYBEL_8:26;
then  K in the carrier of (BoolePoset Y) ;
then A16: K in dom f by FUNCT_2:def_1;
 ex K9 being Subset of L st
( K9 = K & f . K = sup K9 ) by A4, A15;
hence  k in rng f by A14, A16, FUNCT_1:def_3; ::_thesis: verum
end;
then A17: rng f = the carrier of L by XBOOLE_0:def_10;
now__::_thesis:_for_z,_v_being_Element_of_(BoolePoset_Y)_st_f_._z_=_f_._v_holds_
z_=_v
let z, v be Element of (BoolePoset Y); ::_thesis: ( f . z = f . v implies z = v )
assume A18: f . z = f . v ; ::_thesis: z = v
consider z9 being Subset of L such that
A19: z9 = z and
A20: f . z = sup z9 by A4;
consider v9 being Subset of L such that
A21: v9 = v and
A22: f . v = sup v9 by A4;
A23: v9 c= ATOM L by A21, WAYBEL_8:26;
 z9 c= ATOM L by A19, WAYBEL_8:26;
then  ( z c= v & v c= z ) by A1, A19, A20, A21, A22, A23, A18, Th26;
hence  z = v by XBOOLE_0:def_10; ::_thesis: verum
end;
then  f is V13() by WAYBEL_1:def_1;
then  f is isomorphic by A17, A5, WAYBEL_0:66;
then  BoolePoset Y,L are_isomorphic by WAYBEL_1:def_8;
hence  L, BoolePoset Y are_isomorphic by WAYBEL_1:6; ::_thesis: verum
end;

begin

theorem :: WAYBEL15:27
for L being Boolean LATTICE holds
( L is arithmetic iff ex X being set st L, BoolePoset X are_isomorphic )
proof
let L be Boolean LATTICE; ::_thesis: ( L is arithmetic iff ex X being set st L, BoolePoset X are_isomorphic )
hereby  ::_thesis: ( ex X being set st L, BoolePoset X are_isomorphic implies L is arithmetic )
assume A1: L is arithmetic ; ::_thesis: ex X being set st L, BoolePoset X are_isomorphic
then  L opp is continuous by Th9, YELLOW_7:38;
then  L is completely-distributive by A1, WAYBEL_6:39;
then  for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) by Lm5;
hence  ex X being set st L, BoolePoset X are_isomorphic by A1, Lm6; ::_thesis: verum
end;
thus  ( ex X being set st L, BoolePoset X are_isomorphic implies L is arithmetic ) by Th10, WAYBEL_1:6; ::_thesis: verum
end;

theorem :: WAYBEL15:28
for L being Boolean LATTICE holds
( L is arithmetic iff L is algebraic )
proof
let L be Boolean LATTICE; ::_thesis: ( L is arithmetic iff L is algebraic )
thus  ( L is arithmetic implies L is algebraic ) ; ::_thesis: ( L is algebraic implies L is arithmetic )
assume A1: L is algebraic ; ::_thesis: L is arithmetic
then  L opp is continuous by Th9, YELLOW_7:38;
then  L is completely-distributive by A1, WAYBEL_6:39;
then  for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) by Lm5;
then  ex X being set st L, BoolePoset X are_isomorphic by A1, Lm6;
hence  L is arithmetic by Th10, WAYBEL_1:6; ::_thesis: verum
end;

theorem :: WAYBEL15:29
for L being Boolean LATTICE holds
( L is arithmetic iff L is continuous )
proof
let L be Boolean LATTICE; ::_thesis: ( L is arithmetic iff L is continuous )
thus  ( L is arithmetic implies L is continuous ) ; ::_thesis: ( L is continuous implies L is arithmetic )
assume A1: L is continuous ; ::_thesis: L is arithmetic
then  L opp is continuous by Th9, YELLOW_7:38;
then  L is completely-distributive by A1, WAYBEL_6:39;
then  for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) by Lm5;
then  ex X being set st L, BoolePoset X are_isomorphic by A1, Lm6;
hence  L is arithmetic by Th10, WAYBEL_1:6; ::_thesis: verum
end;

theorem :: WAYBEL15:30
for L being Boolean LATTICE holds
( L is arithmetic iff ( L is continuous & L opp is continuous ) )
proof
let L be Boolean LATTICE; ::_thesis: ( L is arithmetic iff ( L is continuous & L opp is continuous ) )
thus  ( L is arithmetic implies ( L is continuous & L opp is continuous ) ) by Th9, YELLOW_7:38; ::_thesis: ( L is continuous & L opp is continuous implies L is arithmetic )
assume that
A1: L is continuous and
A2: L opp is continuous ; ::_thesis: L is arithmetic
 L is completely-distributive by A1, A2, WAYBEL_6:39;
then  for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) by Lm5;
then  ex X being set st L, BoolePoset X are_isomorphic by A1, Lm6;
hence  L is arithmetic by Th10, WAYBEL_1:6; ::_thesis: verum
end;

theorem :: WAYBEL15:31
for L being Boolean LATTICE holds
( L is arithmetic iff L is completely-distributive )
proof
let L be Boolean LATTICE; ::_thesis: ( L is arithmetic iff L is completely-distributive )
thus  ( L is arithmetic implies L is completely-distributive ) ::_thesis: ( L is completely-distributive implies L is arithmetic )
proof
assume A1: L is arithmetic ; ::_thesis: L is completely-distributive
then  L opp is continuous by Th9, YELLOW_7:38;
hence  L is completely-distributive by A1, WAYBEL_6:39; ::_thesis: verum
end;
assume A2: L is completely-distributive ; ::_thesis: L is arithmetic
then  for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) by Lm5;
then  ex X being set st L, BoolePoset X are_isomorphic by A2, Lm6;
hence  L is arithmetic by Th10, WAYBEL_1:6; ::_thesis: verum
end;

theorem :: WAYBEL15:32
for L being Boolean LATTICE holds
( L is arithmetic iff ( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) ) )
proof
let L be Boolean LATTICE; ::_thesis: ( L is arithmetic iff ( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) ) )
hereby  ::_thesis: ( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) implies L is arithmetic )
assume A1: L is arithmetic ; ::_thesis: ( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) )
then  L opp is continuous by Th9, YELLOW_7:38;
then  L is completely-distributive by A1, WAYBEL_6:39;
hence  ( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) ) by Lm5; ::_thesis: verum
end;
assume  ( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) ) ; ::_thesis: L is arithmetic
then  ex X being set st L, BoolePoset X are_isomorphic by Lm6;
hence  L is arithmetic by Th10, WAYBEL_1:6; ::_thesis: verum
end;