:: OPENLATT semantic presentation

begin

registration
cluster non empty Lattice-like lower-bounded Heyting  ->  implicative for LattStr ;
coherence
 for b1 being 0_Lattice st b1 is Heyting holds
b1 is implicative ;
cluster non empty Lattice-like implicative  ->  upper-bounded for LattStr ;
coherence
 for b1 being Lattice st b1 is implicative holds
b1 is upper-bounded ;
end;


theorem Th1: :: OPENLATT:1
for T being TopSpace
for A, B being Subset of T holds A /\ (Int ((A `) \/ B)) c= B
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T holds A /\ (Int ((A `) \/ B)) c= B
let A, B be Subset of T; ::_thesis: A /\ (Int ((A `) \/ B)) c= B
A1: A misses A ` by XBOOLE_1:79;
A /\ ((A `) \/ B) = (A /\ (A `)) \/ (A /\ B) by XBOOLE_1:23
.= {} \/ (A /\ B) by A1, XBOOLE_0:def_7
.= A /\ B ;
then A2: A /\ ((A `) \/ B) c= B by XBOOLE_1:17;
 A /\ (Int ((A `) \/ B)) c= A /\ ((A `) \/ B) by TOPS_1:16, XBOOLE_1:26;
hence  A /\ (Int ((A `) \/ B)) c= B by A2, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th2: :: OPENLATT:2
for T being TopSpace
for A, B, C being Subset of T st C is open & A /\ C c= B holds
C c= Int ((A `) \/ B)
proof
let T be TopSpace; ::_thesis: for A, B, C being Subset of T st C is open & A /\ C c= B holds
C c= Int ((A `) \/ B)
let A, B, C be Subset of T; ::_thesis: ( C is open & A /\ C c= B implies C c= Int ((A `) \/ B) )
assume that
A1: C is open and
A2: A /\ C c= B ; ::_thesis: C c= Int ((A `) \/ B)
A3: C c= C \/ (A `) by XBOOLE_1:7;
(A /\ C) \/ (A `) = (A \/ (A `)) /\ (C \/ (A `)) by XBOOLE_1:24
.= ([#] T) /\ (C \/ (A `)) by PRE_TOPC:2
.= C \/ (A `) by XBOOLE_1:28 ;
then  C \/ (A `) c= B \/ (A `) by A2, XBOOLE_1:9;
then  C c= B \/ (A `) by A3, XBOOLE_1:1;
then  Int C c= Int ((A `) \/ B) by TOPS_1:19;
hence  C c= Int ((A `) \/ B) by A1, TOPS_1:23; ::_thesis: verum
end;

definition
let T be TopStruct ;
func Topology_of T ->  Subset-Family of T equals :: OPENLATT:def 1
 the topology of T;
coherence
 the topology of T is Subset-Family of T ;
end;

:: deftheorem  defines Topology_of OPENLATT:def_1_:_
 for T being TopStruct holds Topology_of T = the topology of T;

registration
let T be TopSpace;
cluster Topology_of T ->  non empty ;
coherence
 not Topology_of T is empty ;
end;

definition
let T be non empty TopSpace;
let P, Q be Element of Topology_of T;
:: original: \/
redefine funcP \/ Q ->  Element of Topology_of T;
coherence
 P \/ Q is Element of Topology_of T
proof
reconsider A = P, B = Q as Subset of T ;
A1: B is open by PRE_TOPC:def_2;
 A is open by PRE_TOPC:def_2;
then  P \/ Q is open by A1;
hence  P \/ Q is Element of Topology_of T by PRE_TOPC:def_2; ::_thesis: verum
end;
:: original: /\
redefine funcP /\ Q ->  Element of Topology_of T;
coherence
 P /\ Q is Element of Topology_of T
proof
reconsider A = P, B = Q as Subset of T ;
A2: B is open by PRE_TOPC:def_2;
 A is open by PRE_TOPC:def_2;
then  P /\ Q is open by A2;
hence  P /\ Q is Element of Topology_of T by PRE_TOPC:def_2; ::_thesis: verum
end;
end;


definition
let T be non empty TopSpace;
func Top_Union T ->  BinOp of (Topology_of T) means :Def2: :: OPENLATT:def 2
 for P, Q being Element of Topology_of T holds it . (P,Q) = P \/ Q;
existence
 ex b1 being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b1 . (P,Q) = P \/ Q
proof
deffunc H1( Element of Topology_of T, Element of Topology_of T) ->  Element of Topology_of T = $1 \/ $2;
thus  ex F being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds F . (P,Q) = H1(P,Q) from BINOP_1:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b1 . (P,Q) = P \/ Q ) & ( for P, Q being Element of Topology_of T holds b2 . (P,Q) = P \/ Q ) holds
b1 = b2
proof
set A = Topology_of T;
deffunc H1( Element of Topology_of T, Element of Topology_of T) ->  Element of Topology_of T = $1 \/ $2;
thus  for o1, o2 being BinOp of (Topology_of T) st ( for a, b being Element of Topology_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Topology_of T holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
func Top_Meet T ->  BinOp of (Topology_of T) means :Def3: :: OPENLATT:def 3
 for P, Q being Element of Topology_of T holds it . (P,Q) = P /\ Q;
existence
 ex b1 being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b1 . (P,Q) = P /\ Q
proof
deffunc H1( Element of Topology_of T, Element of Topology_of T) ->  Element of Topology_of T = $1 /\ $2;
thus  ex F being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds F . (P,Q) = H1(P,Q) from BINOP_1:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b1 . (P,Q) = P /\ Q ) & ( for P, Q being Element of Topology_of T holds b2 . (P,Q) = P /\ Q ) holds
b1 = b2
proof
set A = Topology_of T;
deffunc H1( Element of Topology_of T, Element of Topology_of T) ->  Element of Topology_of T = $1 /\ $2;
thus  for o1, o2 being BinOp of (Topology_of T) st ( for a, b being Element of Topology_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Topology_of T holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Top_Union OPENLATT:def_2_:_
 for T being non empty TopSpace
for b2 being BinOp of (Topology_of T) holds
( b2 = Top_Union T iff for P, Q being Element of Topology_of T holds b2 . (P,Q) = P \/ Q );

:: deftheorem Def3 defines Top_Meet OPENLATT:def_3_:_
 for T being non empty TopSpace
for b2 being BinOp of (Topology_of T) holds
( b2 = Top_Meet T iff for P, Q being Element of Topology_of T holds b2 . (P,Q) = P /\ Q );

theorem Th3: :: OPENLATT:3
for T being non empty TopSpace holds LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice
proof
let T be non empty TopSpace; ::_thesis: LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice
set L = LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #);
A1: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(Topology_of_T),(Top_Union_T),(Top_Meet_T)_#)_holds_p_"\/"_q_=_q_"\/"_p
let p, q be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); ::_thesis: p "\/" q = q "\/" p
thus p "\/" q = q \/ p by Def2
.= q "\/" p by Def2 ; ::_thesis: verum
end;
A2: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(Topology_of_T),(Top_Union_T),(Top_Meet_T)_#)_holds_(p_"/\"_q)_"\/"_q_=_q
let p, q be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); ::_thesis: (p "/\" q) "\/" q = q
thus (p "/\" q) "\/" q = (p "/\" q) \/ q by Def2
.= (p /\ q) \/ q by Def3
.= q by XBOOLE_1:22 ; ::_thesis: verum
end;
A3: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(Topology_of_T),(Top_Union_T),(Top_Meet_T)_#)_holds_p_"/\"_(p_"\/"_q)_=_p
let p, q be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); ::_thesis: p "/\" (p "\/" q) = p
thus p "/\" (p "\/" q) = p /\ (p "\/" q) by Def3
.= p /\ (p \/ q) by Def2
.= p by XBOOLE_1:21 ; ::_thesis: verum
end;
A4: now__::_thesis:_for_p,_q,_r_being_Element_of_LattStr(#_(Topology_of_T),(Top_Union_T),(Top_Meet_T)_#)_holds_p_"/\"_(q_"/\"_r)_=_(p_"/\"_q)_"/\"_r
let p, q, r be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); ::_thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
thus p "/\" (q "/\" r) = p /\ (q "/\" r) by Def3
.= p /\ (q /\ r) by Def3
.= (p /\ q) /\ r by XBOOLE_1:16
.= (p "/\" q) /\ r by Def3
.= (p "/\" q) "/\" r by Def3 ; ::_thesis: verum
end;
A5: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(Topology_of_T),(Top_Union_T),(Top_Meet_T)_#)_holds_p_"/\"_q_=_q_"/\"_p
let p, q be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); ::_thesis: p "/\" q = q "/\" p
thus p "/\" q = q /\ p by Def3
.= q "/\" p by Def3 ; ::_thesis: verum
end;
now__::_thesis:_for_p,_q,_r_being_Element_of_LattStr(#_(Topology_of_T),(Top_Union_T),(Top_Meet_T)_#)_holds_p_"\/"_(q_"\/"_r)_=_(p_"\/"_q)_"\/"_r
let p, q, r be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); ::_thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
thus p "\/" (q "\/" r) = p \/ (q "\/" r) by Def2
.= p \/ (q \/ r) by Def2
.= (p \/ q) \/ r by XBOOLE_1:4
.= (p "\/" q) \/ r by Def2
.= (p "\/" q) "\/" r by Def2 ; ::_thesis: verum
end;
then  ( LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is join-commutative & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is join-associative & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is meet-absorbing & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is meet-commutative & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is meet-associative & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is join-absorbing ) by A1, A2, A5, A4, A3, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence  LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice ; ::_thesis: verum
end;

definition
let T be non empty TopSpace;
func Open_setLatt T ->  Lattice equals :: OPENLATT:def 4
 LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #);
coherence
 LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice by Th3;
end;

:: deftheorem  defines Open_setLatt OPENLATT:def_4_:_
 for T being non empty TopSpace holds Open_setLatt T = LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #);

theorem :: OPENLATT:4
for T being non empty TopSpace holds the carrier of (Open_setLatt T) = Topology_of T ;


theorem :: OPENLATT:5
for T being non empty TopSpace
for p, q being Element of (Open_setLatt T) holds
( p "\/" q = p \/ q & p "/\" q = p /\ q ) by Def2, Def3;

theorem Th6: :: OPENLATT:6
for T being non empty TopSpace
for p, q being Element of (Open_setLatt T) holds
( p [= q iff p c= q )
proof
let T be non empty TopSpace; ::_thesis: for p, q being Element of (Open_setLatt T) holds
( p [= q iff p c= q )
let p, q be Element of (Open_setLatt T); ::_thesis: ( p [= q iff p c= q )
A1: ( p [= q iff p "\/" q = q ) by LATTICES:def_3;
 p "\/" q = p \/ q by Def2;
hence  ( p [= q iff p c= q ) by A1, XBOOLE_1:7, XBOOLE_1:12; ::_thesis: verum
end;

theorem Th7: :: OPENLATT:7
for T being non empty TopSpace
for p, q being Element of (Open_setLatt T)
for p9, q9 being Element of Topology_of T st p = p9 & q = q9 holds
( p [= q iff p9 c= q9 )
proof
let T be non empty TopSpace; ::_thesis: for p, q being Element of (Open_setLatt T)
for p9, q9 being Element of Topology_of T st p = p9 & q = q9 holds
( p [= q iff p9 c= q9 )
let p, q be Element of (Open_setLatt T); ::_thesis: for p9, q9 being Element of Topology_of T st p = p9 & q = q9 holds
( p [= q iff p9 c= q9 )
let p9, q9 be Element of Topology_of T; ::_thesis: ( p = p9 & q = q9 implies ( p [= q iff p9 c= q9 ) )
assume that
A1: p = p9 and
A2: q = q9 ; ::_thesis: ( p [= q iff p9 c= q9 )
hereby  ::_thesis: ( p9 c= q9 implies p [= q )
assume A3: p [= q ; ::_thesis: p9 c= q9
p9 \/ q9 = p "\/" q by A1, A2, Def2
.= q9 by A2, A3, LATTICES:def_3 ;
hence  p9 c= q9 by XBOOLE_1:7; ::_thesis: verum
end;
assume A4: p9 c= q9 ; ::_thesis: p [= q
p "\/" q = p9 \/ q9 by A1, A2, Def2
.= q by A2, A4, XBOOLE_1:12 ;
hence  p [= q by LATTICES:def_3; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
cluster Open_setLatt T ->  implicative ;
coherence
 Open_setLatt T is implicative
proof
set OL = Open_setLatt T;
let p, q be Element of (Open_setLatt T); :: according to FILTER_0:def_6 ::_thesis: ex b1 being Element of the carrier of (Open_setLatt T) st
( p "/\" b1 [= q & ( for b2 being Element of the carrier of (Open_setLatt T) holds
( not p "/\" b2 [= q or b2 [= b1 ) ) )
reconsider p9 = p, q9 = q as Element of Topology_of T ;
reconsider r9 = Int ((p9 `) \/ q9) as Element of Topology_of T by PRE_TOPC:def_2;
reconsider r = r9 as Element of (Open_setLatt T) ;
take  r ; ::_thesis: ( p "/\" r [= q & ( for b1 being Element of the carrier of (Open_setLatt T) holds
( not p "/\" b1 [= q or b1 [= r ) ) )
A1: p "/\" r = p9 /\ r9 by Def3;
 p9 /\ r c= q9 by Th1;
hence  p "/\" r [= q by A1, Th7; ::_thesis: for b1 being Element of the carrier of (Open_setLatt T) holds
( not p "/\" b1 [= q or b1 [= r )
let r1 be Element of (Open_setLatt T); ::_thesis: ( not p "/\" r1 [= q or r1 [= r )
reconsider r2 = r1 as Element of Topology_of T ;
reconsider r19 = r2 as Subset of T ;
A2: r19 is open by PRE_TOPC:def_2;
assume A3: p "/\" r1 [= q ; ::_thesis: r1 [= r
 p "/\" r1 = p9 /\ r19 by Def3;
then  p9 /\ r2 c= q9 by A3, Th7;
then  r19 c= r9 by A2, Th2;
hence  r1 [= r by Th7; ::_thesis: verum
end;
end;

theorem Th8: :: OPENLATT:8
for T being non empty TopSpace holds
( Open_setLatt T is lower-bounded & Bottom (Open_setLatt T) = {} )
proof
let T be non empty TopSpace; ::_thesis: ( Open_setLatt T is lower-bounded & Bottom (Open_setLatt T) = {} )
set OL = Open_setLatt T;
reconsider r = {} as Element of (Open_setLatt T) by PRE_TOPC:1;
A1: now__::_thesis:_for_p_being_Element_of_(Open_setLatt_T)_holds_
(_r_"/\"_p_=_r_&_p_"/\"_r_=_r_)
let p be Element of (Open_setLatt T); ::_thesis: ( r "/\" p = r & p "/\" r = r )
thus r "/\" p = r /\ p by Def3
.= r ; ::_thesis: p "/\" r = r
hence  p "/\" r = r ; ::_thesis: verum
end;
thus  Open_setLatt T is lower-bounded ::_thesis: Bottom (Open_setLatt T) = {}
proof
take  r ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (Open_setLatt T) holds
( r "/\" b1 = r & b1 "/\" r = r )
thus  for b1 being Element of the carrier of (Open_setLatt T) holds
( r "/\" b1 = r & b1 "/\" r = r ) by A1; ::_thesis: verum
end;
hence  Bottom (Open_setLatt T) = {} by A1, LATTICES:def_16; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
cluster Open_setLatt T ->  Heyting ;
coherence
 Open_setLatt T is Heyting
proof
reconsider OL = Open_setLatt T as 0_Lattice by Th8;
 OL is I_Lattice ;
hence  Open_setLatt T is Heyting ; ::_thesis: verum
end;
end;

theorem Th9: :: OPENLATT:9
for T being non empty TopSpace holds Top (Open_setLatt T) = the carrier of T
proof
let T be non empty TopSpace; ::_thesis: Top (Open_setLatt T) = the carrier of T
set OL = Open_setLatt T;
reconsider B = the carrier of T as Element of (Open_setLatt T) by PRE_TOPC:def_1;
now__::_thesis:_for_p_being_Element_of_(Open_setLatt_T)_holds_
(_B_"\/"_p_=_B_&_p_"\/"_B_=_B_)
let p be Element of (Open_setLatt T); ::_thesis: ( B "\/" p = B & p "\/" B = B )
reconsider p9 = p as Element of Topology_of T ;
thus B "\/" p = the carrier of T \/ p9 by Def2
.= B by XBOOLE_1:12 ; ::_thesis: p "\/" B = B
hence  p "\/" B = B ; ::_thesis: verum
end;
hence  Top (Open_setLatt T) = the carrier of T by LATTICES:def_17; ::_thesis: verum
end;


definition
let L be D_Lattice;
func F_primeSet L ->  set  equals :: OPENLATT:def 5
 {  F where F is Filter of L : ( F <> the carrier of L & F is prime )  }  ;
coherence
  {  F where F is Filter of L : ( F <> the carrier of L & F is prime )  }  is set ;
end;

:: deftheorem  defines F_primeSet OPENLATT:def_5_:_
 for L being D_Lattice holds F_primeSet L =  {  F where F is Filter of L : ( F <> the carrier of L & F is prime )  }  ;

theorem Th10: :: OPENLATT:10
for L being D_Lattice
for F being Filter of L holds
( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) )
proof
let L be D_Lattice; ::_thesis: for F being Filter of L holds
( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) )
let F be Filter of L; ::_thesis: ( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) )
 ( F in F_primeSet L iff ex F0 being Filter of L st
( F0 = F & F0 <> the carrier of L & F0 is prime ) ) ;
hence  ( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) ) ; ::_thesis: verum
end;

definition
let L be D_Lattice;
func StoneH L ->  Function means :Def6: :: OPENLATT:def 6
 for a being Element of L holds
( dom it = the carrier of L & it . a =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  );
existence
 ex b1 being Function st
for a being Element of L holds
( dom b1 = the carrier of L & b1 . a =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  )
proof
deffunc H1( set ) ->  set =  {  F where F is Filter of L : ( F in F_primeSet L & $1 in F )  }  ;
consider f being Function such that
A1: ( dom f = the carrier of L & ( for x being set st x in the carrier of L holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
take  f ; ::_thesis: for a being Element of L holds
( dom f = the carrier of L & f . a =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  )
thus  for a being Element of L holds
( dom f = the carrier of L & f . a =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st ( for a being Element of L holds
( dom b1 = the carrier of L & b1 . a =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  ) ) & ( for a being Element of L holds
( dom b2 = the carrier of L & b2 . a =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  ) ) holds
b1 = b2
proof
let f1, f2 be Function; ::_thesis: ( ( for a being Element of L holds
( dom f1 = the carrier of L & f1 . a =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  ) ) & ( for a being Element of L holds
( dom f2 = the carrier of L & f2 . a =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  ) ) implies f1 = f2 )
assume that
A2: for a being Element of L holds
( dom f1 = the carrier of L & f1 . a =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  ) and
A3: for a being Element of L holds
( dom f2 = the carrier of L & f2 . a =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  ) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in the carrier of L implies f1 . x = f2 . x )
assume  x in the carrier of L ; ::_thesis: f1 . x = f2 . x
then reconsider a = x as Element of L ;
thus f1 . x =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  by A2
.= f2 . x by A3 ; ::_thesis: verum
end;
hence  f1 = f2 by A2, A3, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines StoneH OPENLATT:def_6_:_
 for L being D_Lattice
for b2 being Function holds
( b2 = StoneH L iff for a being Element of L holds
( dom b2 = the carrier of L & b2 . a =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  ) );

theorem Th11: :: OPENLATT:11
for L being D_Lattice
for F being Filter of L
for a being Element of L holds
( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) )
proof
let L be D_Lattice; ::_thesis: for F being Filter of L
for a being Element of L holds
( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) )
let F be Filter of L; ::_thesis: for a being Element of L holds
( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) )
let a be Element of L; ::_thesis: ( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) )
 (StoneH L) . a =  {  F0 where F0 is Filter of L : ( F0 in F_primeSet L & a in F0 )  }  by Def6;
then  ( F in (StoneH L) . a iff ex F0 being Filter of L st
( F = F0 & F0 in F_primeSet L & a in F0 ) ) ;
hence  ( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) ) ; ::_thesis: verum
end;

theorem Th12: :: OPENLATT:12
for L being D_Lattice
for a being Element of L
for x being set holds
( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )
proof
let L be D_Lattice; ::_thesis: for a being Element of L
for x being set holds
( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )
let a be Element of L; ::_thesis: for x being set holds
( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )
let x be set ; ::_thesis: ( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )
A1: (StoneH L) . a =  {  F where F is Filter of L : ( F in F_primeSet L & a in F )  }  by Def6;
hereby  ::_thesis: ( ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) implies x in (StoneH L) . a )
assume  x in (StoneH L) . a ; ::_thesis: ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F )
then consider F being Filter of L such that
A2: x = F and
A3: F in F_primeSet L and
A4: a in F by A1;
A5: F is prime by A3, Th10;
 F <> the carrier of L by A3, Th10;
hence  ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) by A2, A4, A5; ::_thesis: verum
end;
given F being Filter of L such that A6: F = x and
A7: F <> the carrier of L and
A8: F is prime and
A9: a in F ; ::_thesis: x in (StoneH L) . a
 F in F_primeSet L by A7, A8;
hence  x in (StoneH L) . a by A1, A6, A9; ::_thesis: verum
end;

definition
let L be D_Lattice;
func StoneS L ->  set  equals :: OPENLATT:def 7
 rng (StoneH L);
coherence
 rng (StoneH L) is set ;
end;

:: deftheorem  defines StoneS OPENLATT:def_7_:_
 for L being D_Lattice holds StoneS L = rng (StoneH L);

registration
let L be D_Lattice;
cluster StoneS L ->  non empty ;
coherence
 not StoneS L is empty
proof
 dom (StoneH L) = the carrier of L by Def6;
hence  not StoneS L is empty by RELAT_1:42; ::_thesis: verum
end;
end;

theorem Th13: :: OPENLATT:13
for L being D_Lattice
for x being set holds
( x in StoneS L iff ex a being Element of L st x = (StoneH L) . a )
proof
let L be D_Lattice; ::_thesis: for x being set holds
( x in StoneS L iff ex a being Element of L st x = (StoneH L) . a )
let x be set ; ::_thesis: ( x in StoneS L iff ex a being Element of L st x = (StoneH L) . a )
hereby  ::_thesis: ( ex a being Element of L st x = (StoneH L) . a implies x in StoneS L )
assume  x in StoneS L ; ::_thesis: ex y being Element of L st x = (StoneH L) . y
then consider y being set  such that
A1: y in dom (StoneH L) and
A2: x = (StoneH L) . y by FUNCT_1:def_3;
reconsider y = y as Element of L by A1, Def6;
take y = y; ::_thesis: x = (StoneH L) . y
thus  x = (StoneH L) . y by A2; ::_thesis: verum
end;
given b being Element of L such that A3: x = (StoneH L) . b ; ::_thesis: x in StoneS L
 b in the carrier of L ;
then  b in dom (StoneH L) by Def6;
hence  x in StoneS L by A3, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th14: :: OPENLATT:14
for L being D_Lattice
for a, b being Element of L holds (StoneH L) . (a "\/" b) = ((StoneH L) . a) \/ ((StoneH L) . b)
proof
let L be D_Lattice; ::_thesis: for a, b being Element of L holds (StoneH L) . (a "\/" b) = ((StoneH L) . a) \/ ((StoneH L) . b)
let a, b be Element of L; ::_thesis: (StoneH L) . (a "\/" b) = ((StoneH L) . a) \/ ((StoneH L) . b)
set c = a "\/" b;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ((StoneH L) . a) \/ ((StoneH L) . b) c= (StoneH L) . (a "\/" b)
set c = a "\/" b;
let x be set ; ::_thesis: ( x in (StoneH L) . (a "\/" b) implies x in ((StoneH L) . a) \/ ((StoneH L) . b) )
assume  x in (StoneH L) . (a "\/" b) ; ::_thesis: x in ((StoneH L) . a) \/ ((StoneH L) . b)
then consider F being Filter of L such that
A1: x = F and
A2: F <> the carrier of L and
A3: F is prime and
A4: a "\/" b in F by Th12;
 ( a in F or b in F ) by A3, A4, FILTER_0:def_5;
then  ( F in (StoneH L) . a or F in (StoneH L) . b ) by A2, A3, Th12;
hence  x in ((StoneH L) . a) \/ ((StoneH L) . b) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((StoneH L) . a) \/ ((StoneH L) . b) or x in (StoneH L) . (a "\/" b) )
assume  x in ((StoneH L) . a) \/ ((StoneH L) . b) ; ::_thesis: x in (StoneH L) . (a "\/" b)
then  ( x in (StoneH L) . a or x in (StoneH L) . b ) by XBOOLE_0:def_3;
then  ( ex F being Filter of L st
( x = F & F <> the carrier of L & F is prime & a in F ) or ex F being Filter of L st
( x = F & F <> the carrier of L & F is prime & b in F ) ) by Th12;
then consider F being Filter of L such that
A5: x = F and
A6: F <> the carrier of L and
A7: F is prime and
A8: ( a in F or b in F ) ;
 a "\/" b in F by A7, A8, FILTER_0:def_5;
hence  x in (StoneH L) . (a "\/" b) by A5, A6, A7, Th12; ::_thesis: verum
end;

theorem Th15: :: OPENLATT:15
for L being D_Lattice
for a, b being Element of L holds (StoneH L) . (a "/\" b) = ((StoneH L) . a) /\ ((StoneH L) . b)
proof
let L be D_Lattice; ::_thesis: for a, b being Element of L holds (StoneH L) . (a "/\" b) = ((StoneH L) . a) /\ ((StoneH L) . b)
let a, b be Element of L; ::_thesis: (StoneH L) . (a "/\" b) = ((StoneH L) . a) /\ ((StoneH L) . b)
set c = a "/\" b;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ((StoneH L) . a) /\ ((StoneH L) . b) c= (StoneH L) . (a "/\" b)
set c = a "/\" b;
let x be set ; ::_thesis: ( x in (StoneH L) . (a "/\" b) implies x in ((StoneH L) . a) /\ ((StoneH L) . b) )
assume  x in (StoneH L) . (a "/\" b) ; ::_thesis: x in ((StoneH L) . a) /\ ((StoneH L) . b)
then consider F being Filter of L such that
A1: x = F and
A2: F <> the carrier of L and
A3: F is prime and
A4: a "/\" b in F by Th12;
 b in F by A4, FILTER_0:8;
then A5: F in (StoneH L) . b by A2, A3, Th12;
 a in F by A4, FILTER_0:8;
then  F in (StoneH L) . a by A2, A3, Th12;
hence  x in ((StoneH L) . a) /\ ((StoneH L) . b) by A1, A5, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((StoneH L) . a) /\ ((StoneH L) . b) or x in (StoneH L) . (a "/\" b) )
assume A6: x in ((StoneH L) . a) /\ ((StoneH L) . b) ; ::_thesis: x in (StoneH L) . (a "/\" b)
then  x in (StoneH L) . b by XBOOLE_0:def_4;
then A7: ex F being Filter of L st
( x = F & F <> the carrier of L & F is prime & b in F ) by Th12;
 x in (StoneH L) . a by A6, XBOOLE_0:def_4;
then  ex F being Filter of L st
( x = F & F <> the carrier of L & F is prime & a in F ) by Th12;
then consider F being Filter of L such that
A8: x = F and
A9: F <> the carrier of L and
A10: F is prime and
A11: a in F and
A12: b in F by A7;
 a "/\" b in F by A11, A12, FILTER_0:8;
hence  x in (StoneH L) . (a "/\" b) by A8, A9, A10, Th12; ::_thesis: verum
end;

definition
let L be D_Lattice;
let a be Element of L;
func SF_have a ->  Subset-Family of L equals :: OPENLATT:def 8
 {  F where F is Filter of L : a in F  }  ;
coherence
  {  F where F is Filter of L : a in F  }  is Subset-Family of L
proof
set A =  {  F where F is Filter of L : a in F  }  ;
  {  F where F is Filter of L : a in F  }  c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F where F is Filter of L : a in F  }  or x in bool the carrier of L )
assume  x in  {  F where F is Filter of L : a in F  }  ; ::_thesis: x in bool the carrier of L
then  ex F being Filter of L st
( x = F & a in F ) ;
hence  x in bool the carrier of L ; ::_thesis: verum
end;
hence   {  F where F is Filter of L : a in F  }  is Subset-Family of L ; ::_thesis: verum
end;
end;

:: deftheorem  defines SF_have OPENLATT:def_8_:_
 for L being D_Lattice
for a being Element of L holds SF_have a =  {  F where F is Filter of L : a in F  }  ;

registration
let L be D_Lattice;
let a be Element of L;
cluster SF_have a ->  non empty ;
coherence
 not SF_have a is empty
proof
 a in <.a.) ;
then  <.a.) in  {  F where F is Filter of L : a in F  }  ;
hence  not SF_have a is empty ; ::_thesis: verum
end;
end;

theorem Th16: :: OPENLATT:16
for L being D_Lattice
for a being Element of L
for x being set holds
( x in SF_have a iff ( x is Filter of L & a in x ) )
proof
let L be D_Lattice; ::_thesis: for a being Element of L
for x being set holds
( x in SF_have a iff ( x is Filter of L & a in x ) )
let a be Element of L; ::_thesis: for x being set holds
( x in SF_have a iff ( x is Filter of L & a in x ) )
let x be set ; ::_thesis: ( x in SF_have a iff ( x is Filter of L & a in x ) )
 ( x in SF_have a iff ex F being Filter of L st
( F = x & a in F ) ) ;
hence  ( x in SF_have a iff ( x is Filter of L & a in x ) ) ; ::_thesis: verum
end;

Lm1:  for L being D_Lattice
for F being Filter of L
for b, a being Element of L holds
( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
proof
let L be D_Lattice; ::_thesis: for F being Filter of L
for b, a being Element of L holds
( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
let F be Filter of L; ::_thesis: for b, a being Element of L holds
( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
let b, a be Element of L; ::_thesis: ( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
 ( F in (SF_have b) \ (SF_have a) iff ( F in SF_have b & not F in SF_have a ) ) by XBOOLE_0:def_5;
hence  ( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) ) by Th16; ::_thesis: verum
end;

theorem Th17: :: OPENLATT:17
for L being D_Lattice
for b, a being Element of L
for x being set st x in (SF_have b) \ (SF_have a) holds
( x is Filter of L & b in x & not a in x )
proof
let L be D_Lattice; ::_thesis: for b, a being Element of L
for x being set st x in (SF_have b) \ (SF_have a) holds
( x is Filter of L & b in x & not a in x )
let b, a be Element of L; ::_thesis: for x being set st x in (SF_have b) \ (SF_have a) holds
( x is Filter of L & b in x & not a in x )
let x be set ; ::_thesis: ( x in (SF_have b) \ (SF_have a) implies ( x is Filter of L & b in x & not a in x ) )
assume A1: x in (SF_have b) \ (SF_have a) ; ::_thesis: ( x is Filter of L & b in x & not a in x )
then A2: not x in SF_have a by XBOOLE_0:def_5;
A3: x in SF_have b by A1, XBOOLE_0:def_5;
then  x is Filter of L by Th16;
hence  ( x is Filter of L & b in x & not a in x ) by A3, A2, Th16; ::_thesis: verum
end;

theorem Th18: :: OPENLATT:18
for L being D_Lattice
for b, a being Element of L
for Z being set st Z <> {} & Z c= (SF_have b) \ (SF_have a) & Z is c=-linear holds
ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
proof
let L be D_Lattice; ::_thesis: for b, a being Element of L
for Z being set st Z <> {} & Z c= (SF_have b) \ (SF_have a) & Z is c=-linear holds
ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
let b, a be Element of L; ::_thesis: for Z being set st Z <> {} & Z c= (SF_have b) \ (SF_have a) & Z is c=-linear holds
ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
let Z be set ; ::_thesis: ( Z <> {} & Z c= (SF_have b) \ (SF_have a) & Z is c=-linear implies ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
assume that
A1: Z <> {} and
A2: Z c= (SF_have b) \ (SF_have a) and
A3: Z is c=-linear ; ::_thesis: ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
reconsider Z = Z as Subset-Family of L by A2, XBOOLE_1:1;
take Y = union Z; ::_thesis: ( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
 Y in (SF_have b) \ (SF_have a)
proof
set X = the Element of Z;
A4: not a in Y
proof
assume  a in Y ; ::_thesis: contradiction
then  ex X being set st
( a in X & X in Z ) by TARSKI:def_4;
hence  contradiction by A2, Th17; ::_thesis: verum
end;
 the Element of Z in (SF_have b) \ (SF_have a) by A1, A2, TARSKI:def_3;
then A5: b in the Element of Z by Th17;
then A6: b in Y by A1, TARSKI:def_4;
reconsider Y = Y as non empty Subset of L by A1, A5, TARSKI:def_4;
now__::_thesis:_for_p,_q_being_Element_of_L_holds_
(_(_p_in_Y_&_q_in_Y_implies_p_"/\"_q_in_Y_)_&_(_p_"/\"_q_in_Y_implies_(_p_in_Y_&_q_in_Y_)_)_)
let p, q be Element of L; ::_thesis: ( ( p in Y & q in Y implies p "/\" q in Y ) & ( p "/\" q in Y implies ( p in Y & q in Y ) ) )
thus  ( p in Y & q in Y implies p "/\" q in Y ) ::_thesis: ( p "/\" q in Y implies ( p in Y & q in Y ) )
proof
assume  p in Y ; ::_thesis: ( not q in Y or p "/\" q in Y )
then consider X1 being set  such that
A7: p in X1 and
A8: X1 in Z by TARSKI:def_4;
A9: X1 is Filter of L by A2, A8, Th17;
assume  q in Y ; ::_thesis: p "/\" q in Y
then consider X2 being set  such that
A10: q in X2 and
A11: X2 in Z by TARSKI:def_4;
 X1,X2 are_c=-comparable by A3, A8, A11, ORDINAL1:def_8;
then A12: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9;
 X2 is Filter of L by A2, A11, Th17;
then  ( p "/\" q in X1 or p "/\" q in X2 ) by A7, A10, A9, A12, FILTER_0:8;
hence  p "/\" q in Y by A8, A11, TARSKI:def_4; ::_thesis: verum
end;
assume  p "/\" q in Y ; ::_thesis: ( p in Y & q in Y )
then consider X1 being set  such that
A13: p "/\" q in X1 and
A14: X1 in Z by TARSKI:def_4;
A15: X1 is Filter of L by A2, A14, Th17;
then A16: q in X1 by A13, FILTER_0:8;
 p in X1 by A13, A15, FILTER_0:8;
hence  ( p in Y & q in Y ) by A14, A16, TARSKI:def_4; ::_thesis: verum
end;
then  Y is Filter of L by FILTER_0:8;
hence  Y in (SF_have b) \ (SF_have a) by A4, A6, Lm1; ::_thesis: verum
end;
hence  ( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by ZFMISC_1:74; ::_thesis: verum
end;

theorem Th19: :: OPENLATT:19
for L being D_Lattice
for b, a being Element of L st not b [= a holds
<.b.) in (SF_have b) \ (SF_have a)
proof
let L be D_Lattice; ::_thesis: for b, a being Element of L st not b [= a holds
<.b.) in (SF_have b) \ (SF_have a)
let b, a be Element of L; ::_thesis: ( not b [= a implies <.b.) in (SF_have b) \ (SF_have a) )
assume  not b [= a ; ::_thesis: <.b.) in (SF_have b) \ (SF_have a)
then  not a in <.b.) by FILTER_0:15;
then A1: not <.b.) in SF_have a by Th16;
 b in <.b.) ;
then  <.b.) in SF_have b ;
hence  <.b.) in (SF_have b) \ (SF_have a) by A1, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th20: :: OPENLATT:20
for L being D_Lattice
for b, a being Element of L st not b [= a holds
ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F )
proof
let L be D_Lattice; ::_thesis: for b, a being Element of L st not b [= a holds
ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F )
let b, a be Element of L; ::_thesis: ( not b [= a implies ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F ) )
set A = (SF_have b) \ (SF_have a);
assume  not b [= a ; ::_thesis: ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F )
then A1: (SF_have b) \ (SF_have a) <> {} by Th19;
 for Z being set st Z <> {} & Z c= (SF_have b) \ (SF_have a) & Z is c=-linear holds
ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by Th18;
then consider Y being set  such that
A2: Y in (SF_have b) \ (SF_have a) and
A3: for Z being set st Z in (SF_have b) \ (SF_have a) & Z <> Y holds
not Y c= Z by A1, LATTICE4:1;
reconsider Y = Y as Filter of L by A2, Th17;
A4: b in Y by A2, Th17;
A5: not a in Y by A2, Th17;
A6: Y is prime
proof
let a1, a2 be Element of L; :: according to FILTER_0:def_5 ::_thesis: ( ( not a1 "\/" a2 in Y or a1 in Y or a2 in Y ) & ( ( not a1 in Y & not a2 in Y ) or a1 "\/" a2 in Y ) )
thus  ( not a1 "\/" a2 in Y or a1 in Y or a2 in Y ) ::_thesis: ( ( not a1 in Y & not a2 in Y ) or a1 "\/" a2 in Y )
proof
set F2 = <.(<.a2.) \/ Y).);
set F1 = <.(<.a1.) \/ Y).);
assume that
A7: a1 "\/" a2 in Y and
A8: not a1 in Y and
A9: not a2 in Y ; ::_thesis: contradiction
A10: <.a1.) c= <.(<.a1.) \/ Y).) by LATTICE4:2;
 a1 in <.a1.) ;
then A11: a1 in <.(<.a1.) \/ Y).) by A10;
A12: Y c= <.(<.a1.) \/ Y).) by LATTICE4:2;
A13: <.a2.) c= <.(<.a2.) \/ Y).) by LATTICE4:2;
 a2 in <.a2.) ;
then A14: a2 in <.(<.a2.) \/ Y).) by A13;
A15: Y c= <.(<.a2.) \/ Y).) by LATTICE4:2;
 ( not a in <.(<.a1.) \/ Y).) or not a in <.(<.a2.) \/ Y).) )
proof
assume that
A16: a in <.(<.a1.) \/ Y).) and
A17: a in <.(<.a2.) \/ Y).) ; ::_thesis: contradiction
consider c1 being Element of L such that
A18: c1 in Y and
A19: a1 "/\" c1 [= a by A16, LATTICE4:3;
consider c2 being Element of L such that
A20: c2 in Y and
A21: a2 "/\" c2 [= a by A17, LATTICE4:3;
set c = c1 "/\" c2;
 a2 "/\" (c1 "/\" c2) [= a2 "/\" c2 by LATTICES:6, LATTICES:9;
then A22: a2 "/\" (c1 "/\" c2) [= a by A21, LATTICES:7;
 a1 "/\" (c1 "/\" c2) [= a1 "/\" c1 by LATTICES:6, LATTICES:9;
then  a1 "/\" (c1 "/\" c2) [= a by A19, LATTICES:7;
then  (a1 "/\" (c1 "/\" c2)) "\/" (a2 "/\" (c1 "/\" c2)) [= a by A22, FILTER_0:6;
then A23: (a1 "\/" a2) "/\" (c1 "/\" c2) [= a by LATTICES:def_11;
 c1 "/\" c2 in Y by A18, A20, FILTER_0:8;
then  (a1 "\/" a2) "/\" (c1 "/\" c2) in Y by A7, FILTER_0:8;
hence  contradiction by A5, A23, FILTER_0:9; ::_thesis: verum
end;
then  ( <.(<.a1.) \/ Y).) in (SF_have b) \ (SF_have a) or <.(<.a2.) \/ Y).) in (SF_have b) \ (SF_have a) ) by A4, A12, A15, Lm1;
hence  contradiction by A3, A8, A9, A11, A14, A12, A15; ::_thesis: verum
end;
thus  ( ( not a1 in Y & not a2 in Y ) or a1 "\/" a2 in Y ) by FILTER_0:10; ::_thesis: verum
end;
 Y <> the carrier of L by A2, Th17;
then  Y in F_primeSet L by A6;
hence  ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F ) by A5, A4; ::_thesis: verum
end;

theorem Th21: :: OPENLATT:21
for L being D_Lattice
for a, b being Element of L st a <> b holds
ex F being Filter of L st F in F_primeSet L
proof
let L be D_Lattice; ::_thesis: for a, b being Element of L st a <> b holds
ex F being Filter of L st F in F_primeSet L
let a, b be Element of L; ::_thesis: ( a <> b implies ex F being Filter of L st F in F_primeSet L )
assume  a <> b ; ::_thesis: ex F being Filter of L st F in F_primeSet L
then  ( not a [= b or not b [= a ) by LATTICES:8;
then  ( ex F being Filter of L st
( F in F_primeSet L & not b in F & a in F ) or ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F ) ) by Th20;
hence  ex F being Filter of L st F in F_primeSet L ; ::_thesis: verum
end;

theorem Th22: :: OPENLATT:22
for L being D_Lattice
for a, b being Element of L st a <> b holds
(StoneH L) . a <> (StoneH L) . b
proof
let L be D_Lattice; ::_thesis: for a, b being Element of L st a <> b holds
(StoneH L) . a <> (StoneH L) . b
let a, b be Element of L; ::_thesis: ( a <> b implies (StoneH L) . a <> (StoneH L) . b )
assume  a <> b ; ::_thesis: (StoneH L) . a <> (StoneH L) . b
then  ( not a [= b or not b [= a ) by LATTICES:8;
then  ( ex F being Filter of L st
( F in F_primeSet L & not b in F & a in F ) or ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F ) ) by Th20;
then consider F being Filter of L such that
A1: F in F_primeSet L and
A2: ( ( b in F & not a in F ) or ( a in F & not b in F ) ) ;
 ( ( F in (StoneH L) . a & not F in (StoneH L) . b ) or ( F in (StoneH L) . b & not F in (StoneH L) . a ) ) by A1, A2, Th11;
hence  (StoneH L) . a <> (StoneH L) . b ; ::_thesis: verum
end;

registration
let L be D_Lattice;
cluster StoneH L ->  one-to-one ;
coherence
 StoneH L is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (StoneH L) or not x2 in dom (StoneH L) or not (StoneH L) . x1 = (StoneH L) . x2 or x1 = x2 )
assume that
A1: x1 in dom (StoneH L) and
A2: x2 in dom (StoneH L) and
A3: (StoneH L) . x1 = (StoneH L) . x2 ; ::_thesis: x1 = x2
reconsider a1 = x1, a2 = x2 as Element of L by A1, A2, Def6;
 a1 = a2 by A3, Th22;
hence  x1 = x2 ; ::_thesis: verum
end;
end;

definition
let L be D_Lattice;
let A, B be Element of StoneS L;
:: original: \/
redefine funcA \/ B ->  Element of StoneS L;
coherence
 A \/ B is Element of StoneS L
proof
consider b being Element of L such that
A1: B = (StoneH L) . b by Th13;
consider a being Element of L such that
A2: A = (StoneH L) . a by Th13;
 A \/ B = (StoneH L) . (a "\/" b) by A2, A1, Th14;
hence  A \/ B is Element of StoneS L by Th13; ::_thesis: verum
end;
:: original: /\
redefine funcA /\ B ->  Element of StoneS L;
coherence
 A /\ B is Element of StoneS L
proof
consider b being Element of L such that
A3: B = (StoneH L) . b by Th13;
consider a being Element of L such that
A4: A = (StoneH L) . a by Th13;
 A /\ B = (StoneH L) . (a "/\" b) by A4, A3, Th15;
hence  A /\ B is Element of StoneS L by Th13; ::_thesis: verum
end;
end;

definition
let L be D_Lattice;
func Set_Union L ->  BinOp of (StoneS L) means :Def9: :: OPENLATT:def 9
 for A, B being Element of StoneS L holds it . (A,B) = A \/ B;
existence
 ex b1 being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b1 . (A,B) = A \/ B
proof
deffunc H1( Element of StoneS L, Element of StoneS L) ->  Element of StoneS L = $1 \/ $2;
thus  ex F being BinOp of (StoneS L) st
for P, Q being Element of StoneS L holds F . (P,Q) = H1(P,Q) from BINOP_1:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b1 . (A,B) = A \/ B ) & ( for A, B being Element of StoneS L holds b2 . (A,B) = A \/ B ) holds
b1 = b2
proof
set A = StoneS L;
deffunc H1( Element of StoneS L, Element of StoneS L) ->  Element of StoneS L = $1 \/ $2;
thus  for o1, o2 being BinOp of (StoneS L) st ( for a, b being Element of StoneS L holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of StoneS L holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
func Set_Meet L ->  BinOp of (StoneS L) means :Def10: :: OPENLATT:def 10
 for A, B being Element of StoneS L holds it . (A,B) = A /\ B;
existence
 ex b1 being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b1 . (A,B) = A /\ B
proof
deffunc H1( Element of StoneS L, Element of StoneS L) ->  Element of StoneS L = $1 /\ $2;
thus  ex F being BinOp of (StoneS L) st
for P, Q being Element of StoneS L holds F . (P,Q) = H1(P,Q) from BINOP_1:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b1 . (A,B) = A /\ B ) & ( for A, B being Element of StoneS L holds b2 . (A,B) = A /\ B ) holds
b1 = b2
proof
set A = StoneS L;
deffunc H1( Element of StoneS L, Element of StoneS L) ->  Element of StoneS L = $1 /\ $2;
thus  for o1, o2 being BinOp of (StoneS L) st ( for a, b being Element of StoneS L holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of StoneS L holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
end;

:: deftheorem Def9 defines Set_Union OPENLATT:def_9_:_
 for L being D_Lattice
for b2 being BinOp of (StoneS L) holds
( b2 = Set_Union L iff for A, B being Element of StoneS L holds b2 . (A,B) = A \/ B );

:: deftheorem Def10 defines Set_Meet OPENLATT:def_10_:_
 for L being D_Lattice
for b2 being BinOp of (StoneS L) holds
( b2 = Set_Meet L iff for A, B being Element of StoneS L holds b2 . (A,B) = A /\ B );

theorem Th23: :: OPENLATT:23
for L being D_Lattice holds LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice
proof
let L be D_Lattice; ::_thesis: LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice
set SL = LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #);
A1: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(StoneS_L),(Set_Union_L),(Set_Meet_L)_#)_holds_p_"\/"_q_=_q_"\/"_p
let p, q be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); ::_thesis: p "\/" q = q "\/" p
thus p "\/" q = q \/ p by Def9
.= q "\/" p by Def9 ; ::_thesis: verum
end;
A2: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(StoneS_L),(Set_Union_L),(Set_Meet_L)_#)_holds_(p_"/\"_q)_"\/"_q_=_q
let p, q be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); ::_thesis: (p "/\" q) "\/" q = q
thus (p "/\" q) "\/" q = (p "/\" q) \/ q by Def9
.= (p /\ q) \/ q by Def10
.= q by XBOOLE_1:22 ; ::_thesis: verum
end;
A3: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(StoneS_L),(Set_Union_L),(Set_Meet_L)_#)_holds_p_"/\"_(p_"\/"_q)_=_p
let p, q be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); ::_thesis: p "/\" (p "\/" q) = p
thus p "/\" (p "\/" q) = p /\ (p "\/" q) by Def10
.= p /\ (p \/ q) by Def9
.= p by XBOOLE_1:21 ; ::_thesis: verum
end;
A4: now__::_thesis:_for_p,_q,_r_being_Element_of_LattStr(#_(StoneS_L),(Set_Union_L),(Set_Meet_L)_#)_holds_p_"/\"_(q_"/\"_r)_=_(p_"/\"_q)_"/\"_r
let p, q, r be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); ::_thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
thus p "/\" (q "/\" r) = p /\ (q "/\" r) by Def10
.= p /\ (q /\ r) by Def10
.= (p /\ q) /\ r by XBOOLE_1:16
.= (p "/\" q) /\ r by Def10
.= (p "/\" q) "/\" r by Def10 ; ::_thesis: verum
end;
A5: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(StoneS_L),(Set_Union_L),(Set_Meet_L)_#)_holds_p_"/\"_q_=_q_"/\"_p
let p, q be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); ::_thesis: p "/\" q = q "/\" p
thus p "/\" q = q /\ p by Def10
.= q "/\" p by Def10 ; ::_thesis: verum
end;
now__::_thesis:_for_p,_q,_r_being_Element_of_LattStr(#_(StoneS_L),(Set_Union_L),(Set_Meet_L)_#)_holds_p_"\/"_(q_"\/"_r)_=_(p_"\/"_q)_"\/"_r
let p, q, r be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); ::_thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
thus p "\/" (q "\/" r) = p \/ (q "\/" r) by Def9
.= p \/ (q \/ r) by Def9
.= (p \/ q) \/ r by XBOOLE_1:4
.= (p "\/" q) \/ r by Def9
.= (p "\/" q) "\/" r by Def9 ; ::_thesis: verum
end;
then  ( LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is join-commutative & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is join-associative & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is meet-absorbing & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is meet-commutative & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is meet-associative & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is join-absorbing ) by A1, A2, A5, A4, A3, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence  LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice ; ::_thesis: verum
end;

definition
let L be D_Lattice;
func StoneLatt L ->  Lattice equals :: OPENLATT:def 11
 LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #);
coherence
 LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice by Th23;
end;

:: deftheorem  defines StoneLatt OPENLATT:def_11_:_
 for L being D_Lattice holds StoneLatt L = LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #);


theorem :: OPENLATT:24
for L being D_Lattice holds the carrier of (StoneLatt L) = StoneS L ;

theorem :: OPENLATT:25
for L being D_Lattice
for p, q being Element of (StoneLatt L) holds
( p "\/" q = p \/ q & p "/\" q = p /\ q ) by Def9, Def10;

theorem :: OPENLATT:26
for L being D_Lattice
for p, q being Element of (StoneLatt L) holds
( p [= q iff p c= q )
proof
let L be D_Lattice; ::_thesis: for p, q being Element of (StoneLatt L) holds
( p [= q iff p c= q )
let p, q be Element of (StoneLatt L); ::_thesis: ( p [= q iff p c= q )
A1: ( p [= q iff p "\/" q = q ) by LATTICES:def_3;
 p "\/" q = p \/ q by Def9;
hence  ( p [= q iff p c= q ) by A1, XBOOLE_1:7, XBOOLE_1:12; ::_thesis: verum
end;

definition
let L be D_Lattice;
:: original: StoneH
redefine func StoneH L ->  Homomorphism of L, StoneLatt L;
coherence
 StoneH L is Homomorphism of L, StoneLatt L
proof
 dom (StoneH L) = the carrier of L by Def6;
then reconsider f = StoneH L as Function of the carrier of L, the carrier of (StoneLatt L) by FUNCT_2:1;
now__::_thesis:_for_a,_b_being_Element_of_L_holds_
(_f_._(a_"\/"_b)_=_(f_._a)_"\/"_(f_._b)_&_f_._(a_"/\"_b)_=_(f_._a)_"/\"_(f_._b)_)
let a, b be Element of L; ::_thesis: ( f . (a "\/" b) = (f . a) "\/" (f . b) & f . (a "/\" b) = (f . a) "/\" (f . b) )
thus f . (a "\/" b) = (f . a) \/ (f . b) by Th14
.= (f . a) "\/" (f . b) by Def9 ; ::_thesis: f . (a "/\" b) = (f . a) "/\" (f . b)
thus f . (a "/\" b) = (f . a) /\ (f . b) by Th15
.= (f . a) "/\" (f . b) by Def10 ; ::_thesis: verum
end;
hence  StoneH L is Homomorphism of L, StoneLatt L by LATTICE4:def_1; ::_thesis: verum
end;
end;

registration
let L be D_Lattice;
cluster StoneH L ->  bijective for Function of L,(StoneLatt L);
coherence
 for b1 being Function of L,(StoneLatt L) st b1 = StoneH L holds
b1 is bijective
proof
now__::_thesis:_(_StoneH_L_is_one-to-one_&_StoneH_L_is_onto_)
thus  StoneH L is one-to-one ; ::_thesis: StoneH L is onto
thus  StoneH L is onto ::_thesis: verum
proof
thus  rng (StoneH L) = the carrier of (StoneLatt L) ; :: according to FUNCT_2:def_3 ::_thesis: verum
end;
end;
hence  for b1 being Function of L,(StoneLatt L) st b1 = StoneH L holds
b1 is bijective by FUNCT_2:def_4; ::_thesis: verum
end;
cluster StoneLatt L ->  distributive ;
coherence
 StoneLatt L is distributive
proof
 StoneH L is onto by FUNCT_2:def_3;
hence  StoneLatt L is distributive by LATTICE4:11; ::_thesis: verum
end;
end;

theorem :: OPENLATT:27
for L being D_Lattice holds L, StoneLatt L are_isomorphic
proof
let L be D_Lattice; ::_thesis: L, StoneLatt L are_isomorphic
take  StoneH L ; :: according to LATTICE4:def_2 ::_thesis: StoneH L is bijective
thus  StoneH L is bijective ; ::_thesis: verum
end;

registration
cluster non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V90() Heyting implicative for LattStr ;
existence
 not for b1 being H_Lattice holds b1 is trivial
proof
set T = the non empty TopSpace;
set OL = Open_setLatt the non empty TopSpace;
 the carrier of the non empty TopSpace = Top (Open_setLatt the non empty TopSpace) by Th9;
then reconsider a = the carrier of the non empty TopSpace as Element of (Open_setLatt the non empty TopSpace) ;
 {} = Bottom (Open_setLatt the non empty TopSpace) by Th8;
then reconsider b = {} as Element of (Open_setLatt the non empty TopSpace) ;
take  Open_setLatt the non empty TopSpace ; ::_thesis: not Open_setLatt the non empty TopSpace is trivial
take  a ; :: according to STRUCT_0:def_10 ::_thesis: not for b1 being Element of the carrier of (Open_setLatt the non empty TopSpace) holds a = b1
take  b ; ::_thesis: not a = b
thus  not a = b ; ::_thesis: verum
end;
end;


theorem Th28: :: OPENLATT:28
for H being non trivial H_Lattice holds (StoneH H) . (Top H) = F_primeSet H
proof
let H be non trivial H_Lattice; ::_thesis: (StoneH H) . (Top H) = F_primeSet H
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: F_primeSet H c= (StoneH H) . (Top H)
let x be set ; ::_thesis: ( x in (StoneH H) . (Top H) implies x in F_primeSet H )
assume  x in (StoneH H) . (Top H) ; ::_thesis: x in F_primeSet H
then  ex F being Filter of H st
( F = x & F <> the carrier of H & F is prime & Top H in F ) by Th12;
hence  x in F_primeSet H ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F_primeSet H or x in (StoneH H) . (Top H) )
assume  x in F_primeSet H ; ::_thesis: x in (StoneH H) . (Top H)
then consider F being Filter of H such that
A1: F = x and
A2: F <> the carrier of H and
A3: F is prime ;
 Top H in F by FILTER_0:11;
hence  x in (StoneH H) . (Top H) by A1, A2, A3, Th12; ::_thesis: verum
end;

theorem Th29: :: OPENLATT:29
for H being non trivial H_Lattice holds (StoneH H) . (Bottom H) = {}
proof
let H be non trivial H_Lattice; ::_thesis: (StoneH H) . (Bottom H) = {}
set x = the Element of (StoneH H) . (Bottom H);
assume  (StoneH H) . (Bottom H) <> {} ; ::_thesis: contradiction
then  ex F being Filter of H st
( F = the Element of (StoneH H) . (Bottom H) & F <> the carrier of H & F is prime & Bottom H in F ) by Th12;
hence  contradiction by FILTER_0:26; ::_thesis: verum
end;

theorem Th30: :: OPENLATT:30
for H being non trivial H_Lattice holds StoneS H c= bool (F_primeSet H)
proof
let H be non trivial H_Lattice; ::_thesis: StoneS H c= bool (F_primeSet H)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in StoneS H or x in bool (F_primeSet H) )
assume  x in StoneS H ; ::_thesis: x in bool (F_primeSet H)
then consider p9 being Element of H such that
A1: x = (StoneH H) . p9 by Th13;
A2: x =  {  F where F is Filter of H : ( F in F_primeSet H & p9 in F )  }  by A1, Def6;
 x c= F_primeSet H
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x or y in F_primeSet H )
assume  y in x ; ::_thesis: y in F_primeSet H
then  ex F being Filter of H st
( y = F & F in F_primeSet H & p9 in F ) by A2;
hence  y in F_primeSet H ; ::_thesis: verum
end;
hence  x in bool (F_primeSet H) ; ::_thesis: verum
end;

registration
let H be non trivial H_Lattice;
cluster F_primeSet H ->  non empty ;
coherence
 not F_primeSet H is empty
proof
 ex p9, q9 being Element of H st p9 <> q9 by STRUCT_0:def_10;
then  ex F being Filter of H st F in F_primeSet H by Th21;
hence  not F_primeSet H is empty ; ::_thesis: verum
end;
end;

definition
let H be non trivial H_Lattice;
func HTopSpace H ->  strict TopStruct  means :Def12: :: OPENLATT:def 12
( the carrier of it = F_primeSet H & the topology of it =  {  (union A) where A is Subset of (StoneS H) : verum  }  );
existence
 ex b1 being strict TopStruct st
( the carrier of b1 = F_primeSet H & the topology of b1 =  {  (union A) where A is Subset of (StoneS H) : verum  }  )
proof
set FS = F_primeSet H;
set top =  {  (union A) where A is Subset of (StoneS H) : verum  }  ;
A1: StoneS H c= bool (F_primeSet H) by Th30;
  {  (union A) where A is Subset of (StoneS H) : verum  }  c= bool (F_primeSet H)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (union A) where A is Subset of (StoneS H) : verum  }  or x in bool (F_primeSet H) )
assume  x in  {  (union A) where A is Subset of (StoneS H) : verum  }  ; ::_thesis: x in bool (F_primeSet H)
then consider A being Subset of (StoneS H) such that
A2: x = union A ;
 A c= bool (F_primeSet H) by A1, XBOOLE_1:1;
then  x c= union (bool (F_primeSet H)) by A2, ZFMISC_1:77;
then  x is Subset of (F_primeSet H) by ZFMISC_1:81;
hence  x in bool (F_primeSet H) ; ::_thesis: verum
end;
then reconsider top =  {  (union A) where A is Subset of (StoneS H) : verum  }  as Subset-Family of (F_primeSet H) ;
take  TopStruct(# (F_primeSet H),top #) ; ::_thesis: ( the carrier of TopStruct(# (F_primeSet H),top #) = F_primeSet H & the topology of TopStruct(# (F_primeSet H),top #) =  {  (union A) where A is Subset of (StoneS H) : verum  }  )
thus  ( the carrier of TopStruct(# (F_primeSet H),top #) = F_primeSet H & the topology of TopStruct(# (F_primeSet H),top #) =  {  (union A) where A is Subset of (StoneS H) : verum  }  ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict TopStruct st the carrier of b1 = F_primeSet H & the topology of b1 =  {  (union A) where A is Subset of (StoneS H) : verum  }  & the carrier of b2 = F_primeSet H & the topology of b2 =  {  (union A) where A is Subset of (StoneS H) : verum  }  holds
b1 = b2 ;
end;

:: deftheorem Def12 defines HTopSpace OPENLATT:def_12_:_
 for H being non trivial H_Lattice
for b2 being strict TopStruct holds
( b2 = HTopSpace H iff ( the carrier of b2 = F_primeSet H & the topology of b2 =  {  (union A) where A is Subset of (StoneS H) : verum  }  ) );

registration
let H be non trivial H_Lattice;
cluster HTopSpace H ->  non empty strict TopSpace-like ;
coherence
 ( not HTopSpace H is empty & HTopSpace H is TopSpace-like )
proof
reconsider A1 = {((StoneH H) . (Top H))} as Subset of (StoneS H) ;
set TS = HTopSpace H;
A1: the topology of (HTopSpace H) =  {  (union A) where A is Subset of (StoneS H) : verum  }  by Def12;
A2: the carrier of (HTopSpace H) = F_primeSet H by Def12;
hence  not HTopSpace H is empty ; ::_thesis: HTopSpace H is TopSpace-like
 F_primeSet H = (StoneH H) . (Top H) by Th28;
then  F_primeSet H = union A1 by ZFMISC_1:25;
hence  the carrier of (HTopSpace H) in the topology of (HTopSpace H) by A2, A1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of K19(K19( the carrier of (HTopSpace H))) holds
( not b1 c= the topology of (HTopSpace H) or union b1 in the topology of (HTopSpace H) ) ) & ( for b1, b2 being Element of K19( the carrier of (HTopSpace H)) holds
( not b1 in the topology of (HTopSpace H) or not b2 in the topology of (HTopSpace H) or b1 /\ b2 in the topology of (HTopSpace H) ) ) )
hereby  ::_thesis: for b1, b2 being Element of K19( the carrier of (HTopSpace H)) holds
( not b1 in the topology of (HTopSpace H) or not b2 in the topology of (HTopSpace H) or b1 /\ b2 in the topology of (HTopSpace H) )
let a be Subset-Family of (HTopSpace H); ::_thesis: ( a c= the topology of (HTopSpace H) implies union a in the topology of (HTopSpace H) )
defpred S1[ set ] means  union H in a;
set B =  {  A where A is Subset of (StoneS H) : S1[A]  }  ;
set X =  {  (union A) where A is Subset of (StoneS H) : A in  {  A where A is Subset of (StoneS H) : S1[A]  }   }  ;
assume A3: a c= the topology of (HTopSpace H) ; ::_thesis: union a in the topology of (HTopSpace H)
A4: a =  {  (union A) where A is Subset of (StoneS H) : A in  {  A where A is Subset of (StoneS H) : S1[A]  }   }
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  (union A) where A is Subset of (StoneS H) : A in  {  A where A is Subset of (StoneS H) : S1[A]  }   }  c= a
let x be set ; ::_thesis: ( x in a implies x in  {  (union A) where A is Subset of (StoneS H) : A in  {  A where A is Subset of (StoneS H) : S1[A]  }   }  )
assume A5: x in a ; ::_thesis: x in  {  (union A) where A is Subset of (StoneS H) : A in  {  A where A is Subset of (StoneS H) : S1[A]  }   }
then  x in the topology of (HTopSpace H) by A3;
then consider A being Subset of (StoneS H) such that
A6: x = union A by A1;
 A in  {  A where A is Subset of (StoneS H) : S1[A]  }  by A5, A6;
hence  x in  {  (union A) where A is Subset of (StoneS H) : A in  {  A where A is Subset of (StoneS H) : S1[A]  }   }  by A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (union A) where A is Subset of (StoneS H) : A in  {  A where A is Subset of (StoneS H) : S1[A]  }   }  or x in a )
assume  x in  {  (union A) where A is Subset of (StoneS H) : A in  {  A where A is Subset of (StoneS H) : S1[A]  }   }  ; ::_thesis: x in a
then consider A being Subset of (StoneS H) such that
A7: x = union A and
A8: A in  {  A where A is Subset of (StoneS H) : S1[A]  }  ;
 ex A9 being Subset of (StoneS H) st
( A = A9 & union A9 in a ) by A8;
hence  x in a by A7; ::_thesis: verum
end;
reconsider B =  {  A where A is Subset of (StoneS H) : S1[A]  }  as Subset-Family of (StoneS H) from DOMAIN_1:sch_7();
 union (union B) = union a by A4, EQREL_1:54;
hence  union a in the topology of (HTopSpace H) by A1; ::_thesis: verum
end;
let a, b be Subset of (HTopSpace H); ::_thesis: ( not a in the topology of (HTopSpace H) or not b in the topology of (HTopSpace H) or a /\ b in the topology of (HTopSpace H) )
assume that
A9: a in the topology of (HTopSpace H) and
A10: b in the topology of (HTopSpace H) ; ::_thesis: a /\ b in the topology of (HTopSpace H)
consider A being Subset of (StoneS H) such that
A11: a = union A by A1, A9;
consider B being Subset of (StoneS H) such that
A12: b = union B by A1, A10;
 INTERSECTION (A,B) c= StoneS H
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in INTERSECTION (A,B) or x in StoneS H )
assume  x in INTERSECTION (A,B) ; ::_thesis: x in StoneS H
then consider X, Y being set  such that
A13: X in A and
A14: Y in B and
A15: x = X /\ Y by SETFAM_1:def_5;
consider p9 being Element of H such that
A16: X = (StoneH H) . p9 by A13, Th13;
consider q9 being Element of H such that
A17: Y = (StoneH H) . q9 by A14, Th13;
 x = (StoneH H) . (p9 "/\" q9) by A15, A16, A17, Th15;
hence  x in StoneS H ; ::_thesis: verum
end;
then reconsider C = INTERSECTION (A,B) as Subset of (StoneS H) ;
 (union A) /\ (union B) = union C by SETFAM_1:28;
hence  a /\ b in the topology of (HTopSpace H) by A1, A11, A12; ::_thesis: verum
end;
end;

theorem :: OPENLATT:31
for H being non trivial H_Lattice holds the carrier of (Open_setLatt (HTopSpace H)) =  {  (union A) where A is Subset of (StoneS H) : verum  }  by Def12;

theorem Th32: :: OPENLATT:32
for H being non trivial H_Lattice holds StoneS H c= the carrier of (Open_setLatt (HTopSpace H))
proof
let H be non trivial H_Lattice; ::_thesis: StoneS H c= the carrier of (Open_setLatt (HTopSpace H))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in StoneS H or x in the carrier of (Open_setLatt (HTopSpace H)) )
set carrO = the carrier of (Open_setLatt (HTopSpace H));
assume  x in StoneS H ; ::_thesis: x in the carrier of (Open_setLatt (HTopSpace H))
then reconsider z = {x} as Subset of (StoneS H) by ZFMISC_1:31;
A1: union z = x by ZFMISC_1:25;
 the carrier of (Open_setLatt (HTopSpace H)) =  {  (union A) where A is Subset of (StoneS H) : verum  }  by Def12;
hence  x in the carrier of (Open_setLatt (HTopSpace H)) by A1; ::_thesis: verum
end;

definition
let H be non trivial H_Lattice;
:: original: StoneH
redefine func StoneH H ->  Homomorphism of H, Open_setLatt (HTopSpace H);
coherence
 StoneH H is Homomorphism of H, Open_setLatt (HTopSpace H)
proof
set LH = Open_setLatt (HTopSpace H);
reconsider g = StoneH H as Function of the carrier of H, the carrier of (StoneLatt H) ;
 StoneS H c= the carrier of (Open_setLatt (HTopSpace H)) by Th32;
then reconsider f = g as Function of the carrier of H, the carrier of (Open_setLatt (HTopSpace H)) by FUNCT_2:6;
now__::_thesis:_for_p9,_q9_being_Element_of_H_holds_
(_f_._(p9_"\/"_q9)_=_(f_._p9)_"\/"_(f_._q9)_&_f_._(p9_"/\"_q9)_=_(f_._p9)_"/\"_(f_._q9)_)
let p9, q9 be Element of H; ::_thesis: ( f . (p9 "\/" q9) = (f . p9) "\/" (f . q9) & f . (p9 "/\" q9) = (f . p9) "/\" (f . q9) )
thus f . (p9 "\/" q9) = ((StoneH H) . p9) \/ ((StoneH H) . q9) by Th14
.= (f . p9) "\/" (f . q9) by Def2 ; ::_thesis: f . (p9 "/\" q9) = (f . p9) "/\" (f . q9)
thus f . (p9 "/\" q9) = ((StoneH H) . p9) /\ ((StoneH H) . q9) by Th15
.= (f . p9) "/\" (f . q9) by Def3 ; ::_thesis: verum
end;
hence  StoneH H is Homomorphism of H, Open_setLatt (HTopSpace H) by LATTICE4:def_1; ::_thesis: verum
end;
end;

theorem Th33: :: OPENLATT:33
for H being non trivial H_Lattice
for p9, q9 being Element of H holds (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9)
proof
let H be non trivial H_Lattice; ::_thesis: for p9, q9 being Element of H holds (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9)
let p9, q9 be Element of H; ::_thesis: (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9)
A1: the carrier of (Open_setLatt (HTopSpace H)) =  {  (union A) where A is Subset of (StoneS H) : verum  }  by Def12;
A2: now__::_thesis:_for_r_being_Element_of_(Open_setLatt_(HTopSpace_H))_st_((StoneH_H)_._p9)_"/\"_r_[=_(StoneH_H)_._q9_holds_
r_[=_(StoneH_H)_._(p9_=>_q9)
let r be Element of (Open_setLatt (HTopSpace H)); ::_thesis: ( ((StoneH H) . p9) "/\" r [= (StoneH H) . q9 implies r [= (StoneH H) . (p9 => q9) )
 r in the carrier of (Open_setLatt (HTopSpace H)) ;
then consider A being Subset of (StoneS H) such that
A3: r = union A by A1;
assume  ((StoneH H) . p9) "/\" r [= (StoneH H) . q9 ; ::_thesis: r [= (StoneH H) . (p9 => q9)
then  ((StoneH H) . p9) "/\" r c= (StoneH H) . q9 by Th6;
then  ((StoneH H) . p9) /\ (union A) c= (StoneH H) . q9 by A3, Def3;
then A4: union (INTERSECTION ({((StoneH H) . p9)},A)) c= (StoneH H) . q9 by SETFAM_1:25;
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
x_c=_(StoneH_H)_._(p9_=>_q9)
let x be set ; ::_thesis: ( x in A implies x c= (StoneH H) . (p9 => q9) )
assume A5: x in A ; ::_thesis: x c= (StoneH H) . (p9 => q9)
then consider x9 being Element of H such that
A6: x = (StoneH H) . x9 by Th13;
 (StoneH H) . p9 in {((StoneH H) . p9)} by TARSKI:def_1;
then  ((StoneH H) . p9) /\ x in INTERSECTION ({((StoneH H) . p9)},A) by A5, SETFAM_1:def_5;
then  ((StoneH H) . p9) /\ ((StoneH H) . x9) c= (StoneH H) . q9 by A4, A6, SETFAM_1:41;
then  (StoneH H) . (p9 "/\" x9) c= (StoneH H) . q9 by Th15;
then  (StoneH H) . (p9 "/\" x9) [= (StoneH H) . q9 by Th6;
then  p9 "/\" x9 [= q9 by LATTICE4:5;
then  x9 [= p9 => q9 by FILTER_0:def_7;
then  (StoneH H) . x9 [= (StoneH H) . (p9 => q9) by LATTICE4:4;
hence  x c= (StoneH H) . (p9 => q9) by A6, Th6; ::_thesis: verum
end;
then  union A c= (StoneH H) . (p9 => q9) by ZFMISC_1:76;
hence  r [= (StoneH H) . (p9 => q9) by A3, Th6; ::_thesis: verum
end;
 p9 "/\" (p9 => q9) [= q9 by FILTER_0:def_7;
then  (StoneH H) . (p9 "/\" (p9 => q9)) [= (StoneH H) . q9 by LATTICE4:4;
then  ((StoneH H) . p9) "/\" ((StoneH H) . (p9 => q9)) [= (StoneH H) . q9 by LATTICE4:def_1;
hence  (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9) by A2, FILTER_0:def_7; ::_thesis: verum
end;

theorem :: OPENLATT:34
for H being non trivial H_Lattice holds StoneH H preserves_implication
proof
let H be non trivial H_Lattice; ::_thesis: StoneH H preserves_implication
 for p9, q9 being Element of H holds (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9) by Th33;
hence  StoneH H preserves_implication by LATTICE4:def_3; ::_thesis: verum
end;

theorem :: OPENLATT:35
for H being non trivial H_Lattice holds StoneH H preserves_top
proof
let H be non trivial H_Lattice; ::_thesis: StoneH H preserves_top
(StoneH H) . (Top H) = F_primeSet H by Th28
.= the carrier of (HTopSpace H) by Def12
.= Top (Open_setLatt (HTopSpace H)) by Th9 ;
hence  StoneH H preserves_top by LATTICE4:def_4; ::_thesis: verum
end;

theorem :: OPENLATT:36
for H being non trivial H_Lattice holds StoneH H preserves_bottom
proof
let H be non trivial H_Lattice; ::_thesis: StoneH H preserves_bottom
(StoneH H) . (Bottom H) = {} by Th29
.= Bottom (Open_setLatt (HTopSpace H)) by Th8 ;
hence  StoneH H preserves_bottom by LATTICE4:def_5; ::_thesis: verum
end;