:: LOPCLSET semantic presentation

begin


definition
let T be non empty TopStruct ;
func OpenClosedSet T ->  Subset-Family of T equals :: LOPCLSET:def 1
 {  x where x is Subset of T : ( x is open & x is closed )  }  ;
coherence
  {  x where x is Subset of T : ( x is open & x is closed )  }  is Subset-Family of T
proof
set A =  {  x where x is Subset of T : ( x is open & x is closed )  }  ;
  {  x where x is Subset of T : ( x is open & x is closed )  }  c= bool the carrier of T
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  x where x is Subset of T : ( x is open & x is closed )  }  or y in bool the carrier of T )
assume  y in  {  x where x is Subset of T : ( x is open & x is closed )  }  ; ::_thesis: y in bool the carrier of T
then  ex x being Subset of T st
( y = x & x is open & x is closed ) ;
hence  y in bool the carrier of T ; ::_thesis: verum
end;
hence   {  x where x is Subset of T : ( x is open & x is closed )  }  is Subset-Family of T ; ::_thesis: verum
end;
end;

:: deftheorem  defines OpenClosedSet LOPCLSET:def_1_:_
 for T being non empty TopStruct holds OpenClosedSet T =  {  x where x is Subset of T : ( x is open & x is closed )  }  ;

registration
let T be non empty TopSpace;
cluster OpenClosedSet T ->  non empty ;
coherence
 not OpenClosedSet T is empty
proof
set A =  {  x where x is Subset of T : ( x is open & x is closed )  }  ;
 {} T in  {  x where x is Subset of T : ( x is open & x is closed )  }  ;
hence  not OpenClosedSet T is empty ; ::_thesis: verum
end;
end;

theorem Th1: :: LOPCLSET:1
for T being non empty TopSpace
for X being Subset of T st X in OpenClosedSet T holds
X is open
proof
let T be non empty TopSpace; ::_thesis: for X being Subset of T st X in OpenClosedSet T holds
X is open
let X be Subset of T; ::_thesis: ( X in OpenClosedSet T implies X is open )
assume  X in OpenClosedSet T ; ::_thesis: X is open
then  ex Z being Subset of T st
( Z = X & Z is open & Z is closed ) ;
hence  X is open ; ::_thesis: verum
end;

theorem Th2: :: LOPCLSET:2
for T being non empty TopSpace
for X being Subset of T st X in OpenClosedSet T holds
X is closed
proof
let T be non empty TopSpace; ::_thesis: for X being Subset of T st X in OpenClosedSet T holds
X is closed
let X be Subset of T; ::_thesis: ( X in OpenClosedSet T implies X is closed )
assume  X in OpenClosedSet T ; ::_thesis: X is closed
then  ex Z being Subset of T st
( Z = X & Z is open & Z is closed ) ;
hence  X is closed ; ::_thesis: verum
end;

theorem Th3: :: LOPCLSET:3
for T being non empty TopSpace
for X being Subset of T st X is open & X is closed holds
X in OpenClosedSet T ;


definition
let T be non empty TopSpace;
let C, D be Element of OpenClosedSet T;
:: original: \/
redefine funcC \/ D ->  Element of OpenClosedSet T;
coherence
 C \/ D is Element of OpenClosedSet T
proof
reconsider A = C, B = D as Subset of T ;
A1: A is open by Th1;
A2: B is open by Th1;
A3: A is closed by Th2;
A4: B is closed by Th2;
 A \/ B is open by A1, A2;
hence  C \/ D is Element of OpenClosedSet T by A3, A4, Th3; ::_thesis: verum
end;
:: original: /\
redefine funcC /\ D ->  Element of OpenClosedSet T;
coherence
 C /\ D is Element of OpenClosedSet T
proof
reconsider A = C, B = D as Subset of T ;
A5: A is open by Th1;
A6: B is open by Th1;
A7: A is closed by Th2;
A8: B is closed by Th2;
 A /\ B is open by A5, A6;
hence  C /\ D is Element of OpenClosedSet T by A7, A8, Th3; ::_thesis: verum
end;
end;

definition
let T be non empty TopSpace;
deffunc H1( Element of OpenClosedSet T, Element of OpenClosedSet T) ->  Element of OpenClosedSet T = $1 \/ $2;
func T_join T ->  BinOp of (OpenClosedSet T) means :Def2: :: LOPCLSET:def 2
 for A, B being Element of OpenClosedSet T holds it . (A,B) = A \/ B;
existence
 ex b1 being BinOp of (OpenClosedSet T) st
for A, B being Element of OpenClosedSet T holds b1 . (A,B) = A \/ B
proof
consider f being BinOp of (OpenClosedSet T) such that
A1: for x, y being Element of OpenClosedSet T holds f . (x,y) = H1(x,y) from BINOP_1:sch_4();
take  f ; ::_thesis: for A, B being Element of OpenClosedSet T holds f . (A,B) = A \/ B
let x, y be Element of OpenClosedSet T; ::_thesis: f . (x,y) = x \/ y
thus  f . (x,y) = x \/ y by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b1 . (A,B) = A \/ B ) & ( for A, B being Element of OpenClosedSet T holds b2 . (A,B) = A \/ B ) holds
b1 = b2
proof
thus  for b1, b2 being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b1 . (A,B) = H1(A,B) ) & ( for A, B being Element of OpenClosedSet T holds b2 . (A,B) = H1(A,B) ) holds
b1 = b2 from BINOP_2:sch_2(); ::_thesis: verum
end;
deffunc H2( Element of OpenClosedSet T, Element of OpenClosedSet T) ->  Element of OpenClosedSet T = $1 /\ $2;
func T_meet T ->  BinOp of (OpenClosedSet T) means :Def3: :: LOPCLSET:def 3
 for A, B being Element of OpenClosedSet T holds it . (A,B) = A /\ B;
existence
 ex b1 being BinOp of (OpenClosedSet T) st
for A, B being Element of OpenClosedSet T holds b1 . (A,B) = A /\ B
proof
consider f being BinOp of (OpenClosedSet T) such that
A2: for x, y being Element of OpenClosedSet T holds f . (x,y) = H2(x,y) from BINOP_1:sch_4();
take  f ; ::_thesis: for A, B being Element of OpenClosedSet T holds f . (A,B) = A /\ B
let x, y be Element of OpenClosedSet T; ::_thesis: f . (x,y) = x /\ y
thus  f . (x,y) = x /\ y by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b1 . (A,B) = A /\ B ) & ( for A, B being Element of OpenClosedSet T holds b2 . (A,B) = A /\ B ) holds
b1 = b2
proof
thus  for b1, b2 being BinOp of (OpenClosedSet T) st ( for A, B being Element of OpenClosedSet T holds b1 . (A,B) = H2(A,B) ) & ( for A, B being Element of OpenClosedSet T holds b2 . (A,B) = H2(A,B) ) holds
b1 = b2 from BINOP_2:sch_2(); ::_thesis: verum
end;
end;

:: deftheorem Def2 defines T_join LOPCLSET:def_2_:_
 for T being non empty TopSpace
for b2 being BinOp of (OpenClosedSet T) holds
( b2 = T_join T iff for A, B being Element of OpenClosedSet T holds b2 . (A,B) = A \/ B );

:: deftheorem Def3 defines T_meet LOPCLSET:def_3_:_
 for T being non empty TopSpace
for b2 being BinOp of (OpenClosedSet T) holds
( b2 = T_meet T iff for A, B being Element of OpenClosedSet T holds b2 . (A,B) = A /\ B );

theorem :: LOPCLSET:4
for T being non empty TopSpace
for x, y being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #)
for x9, y9 being Element of OpenClosedSet T st x = x9 & y = y9 holds
x "\/" y = x9 \/ y9 by Def2;

theorem :: LOPCLSET:5
for T being non empty TopSpace
for x, y being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #)
for x9, y9 being Element of OpenClosedSet T st x = x9 & y = y9 holds
x "/\" y = x9 /\ y9 by Def3;

theorem :: LOPCLSET:6
for T being non empty TopSpace holds {} T is Element of OpenClosedSet T by Th3;

theorem :: LOPCLSET:7
for T being non empty TopSpace holds [#] T is Element of OpenClosedSet T by Th3;

theorem Th8: :: LOPCLSET:8
for T being non empty TopSpace
for x being Element of OpenClosedSet T holds x ` is Element of OpenClosedSet T
proof
let T be non empty TopSpace; ::_thesis: for x being Element of OpenClosedSet T holds x ` is Element of OpenClosedSet T
let x be Element of OpenClosedSet T; ::_thesis: x ` is Element of OpenClosedSet T
reconsider y = x as Subset of T ;
A1: y is open by Th1;
 y is closed by Th2;
then A2: x ` is open ;
 x ` is closed by A1;
hence  x ` is Element of OpenClosedSet T by A2, Th3; ::_thesis: verum
end;

theorem Th9: :: LOPCLSET:9
for T being non empty TopSpace holds LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice
proof
let T be non empty TopSpace; ::_thesis: LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice
set L = LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #);
A1: for p, q being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "\/" q = q "\/" p
proof
let p, q be Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #); ::_thesis: p "\/" q = q "\/" p
consider p9, q9 being Element of OpenClosedSet T such that
A2: p = p9 and
A3: q = q9 ;
thus p "\/" q = q9 \/ p9 by A2, A3, Def2
.= q "\/" p by A2, A3, Def2 ; ::_thesis: verum
end;
A4: for p, q, r being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "\/" (q "\/" r) = (p "\/" q) "\/" r
proof
let p, q, r be Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #); ::_thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
consider p9, q9, r9, k9, l9 being Element of OpenClosedSet T such that
A5: p = p9 and
A6: q = q9 and
A7: r = r9 and
A8: q "\/" r = k9 and
A9: p "\/" q = l9 ;
thus p "\/" (q "\/" r) = p9 \/ k9 by A5, A8, Def2
.= p9 \/ (q9 \/ r9) by A6, A7, A8, Def2
.= (p9 \/ q9) \/ r9 by XBOOLE_1:4
.= l9 \/ r9 by A5, A6, A9, Def2
.= (p "\/" q) "\/" r by A7, A9, Def2 ; ::_thesis: verum
end;
A10: for p, q being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds (p "/\" q) "\/" q = q
proof
let p, q be Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #); ::_thesis: (p "/\" q) "\/" q = q
consider p9, q9, k9 being Element of OpenClosedSet T such that
A11: p = p9 and
A12: q = q9 and
A13: p "/\" q = k9 ;
thus (p "/\" q) "\/" q = k9 \/ q9 by A12, A13, Def2
.= (p9 /\ q9) \/ q9 by A11, A12, A13, Def3
.= q by A12, XBOOLE_1:22 ; ::_thesis: verum
end;
A14: for p, q being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "/\" q = q "/\" p
proof
let p, q be Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #); ::_thesis: p "/\" q = q "/\" p
consider p9, q9 being Element of OpenClosedSet T such that
A15: p = p9 and
A16: q = q9 ;
thus p "/\" q = q9 /\ p9 by A15, A16, Def3
.= q "/\" p by A15, A16, Def3 ; ::_thesis: verum
end;
A17: for p, q, r being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "/\" (q "/\" r) = (p "/\" q) "/\" r
proof
let p, q, r be Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #); ::_thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
consider p9, q9, r9, k9, l9 being Element of OpenClosedSet T such that
A18: p = p9 and
A19: q = q9 and
A20: r = r9 and
A21: q "/\" r = k9 and
A22: p "/\" q = l9 ;
thus p "/\" (q "/\" r) = p9 /\ k9 by A18, A21, Def3
.= p9 /\ (q9 /\ r9) by A19, A20, A21, Def3
.= (p9 /\ q9) /\ r9 by XBOOLE_1:16
.= l9 /\ r9 by A18, A19, A22, Def3
.= (p "/\" q) "/\" r by A20, A22, Def3 ; ::_thesis: verum
end;
 for p, q being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "/\" (p "\/" q) = p
proof
let p, q be Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #); ::_thesis: p "/\" (p "\/" q) = p
consider p9, q9, k9 being Element of OpenClosedSet T such that
A23: p = p9 and
A24: q = q9 and
A25: p "\/" q = k9 ;
thus p "/\" (p "\/" q) = p9 /\ k9 by A23, A25, Def3
.= p9 /\ (p9 \/ q9) by A23, A24, A25, Def2
.= p by A23, XBOOLE_1:21 ; ::_thesis: verum
end;
then  ( LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is join-commutative & LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is join-associative & LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is meet-absorbing & LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is meet-commutative & LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is meet-associative & LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is join-absorbing ) by A1, A4, A10, A14, A17, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence  LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice ; ::_thesis: verum
end;

definition
let T be non empty TopSpace;
func OpenClosedSetLatt T ->  Lattice equals :: LOPCLSET:def 4
 LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #);
coherence
 LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice by Th9;
end;

:: deftheorem  defines OpenClosedSetLatt LOPCLSET:def_4_:_
 for T being non empty TopSpace holds OpenClosedSetLatt T = LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #);

theorem :: LOPCLSET:10
for T being non empty TopSpace
for x, y being Element of (OpenClosedSetLatt T) holds x "\/" y = x \/ y by Def2;

theorem :: LOPCLSET:11
for T being non empty TopSpace
for x, y being Element of (OpenClosedSetLatt T) holds x "/\" y = x /\ y by Def3;

theorem :: LOPCLSET:12
for T being non empty TopSpace holds the carrier of (OpenClosedSetLatt T) = OpenClosedSet T ;

registration
let T be non empty TopSpace;
cluster OpenClosedSetLatt T ->  Boolean ;
coherence
 OpenClosedSetLatt T is Boolean
proof
set OCL = OpenClosedSetLatt T;
A1: for a, b, c being Element of (OpenClosedSetLatt T) holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
proof
let a, b, c be Element of (OpenClosedSetLatt T); ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
set m = a "/\" c;
consider a9, b9, c9, k9, l9, m9 being Element of OpenClosedSet T such that
A2: a = a9 and
A3: b = b9 and
A4: c = c9 and
A5: b "\/" c = k9 and
A6: a "/\" b = l9 and
A7: a "/\" c = m9 ;
A8: a9 /\ c9 = a "/\" c by A2, A4, Def3;
thus a "/\" (b "\/" c) = a9 /\ k9 by A2, A5, Def3
.= a9 /\ (b9 \/ c9) by A3, A4, A5, Def2
.= (a9 /\ b9) \/ (a9 /\ c9) by XBOOLE_1:23
.= l9 \/ m9 by A2, A3, A6, A7, A8, Def3
.= (a "/\" b) "\/" (a "/\" c) by A6, A7, Def2 ; ::_thesis: verum
end;
reconsider bot = {} T as Element of (OpenClosedSetLatt T) by Th3;
reconsider top = [#] T as Element of (OpenClosedSetLatt T) by Th3;
A9: for a being Element of (OpenClosedSetLatt T) holds
( top "\/" a = top & a "\/" top = top )
proof
let a be Element of (OpenClosedSetLatt T); ::_thesis: ( top "\/" a = top & a "\/" top = top )
reconsider a9 = a as Element of OpenClosedSet T ;
thus top "\/" a = ([#] T) \/ a9 by Def2
.= top by XBOOLE_1:12 ; ::_thesis: a "\/" top = top
hence  a "\/" top = top ; ::_thesis: verum
end;
A10: for a being Element of (OpenClosedSetLatt T) holds
( bot "/\" a = bot & a "/\" bot = bot )
proof
let a be Element of (OpenClosedSetLatt T); ::_thesis: ( bot "/\" a = bot & a "/\" bot = bot )
reconsider a9 = a as Element of OpenClosedSet T ;
thus bot "/\" a = {} /\ a9 by Def3
.= bot ; ::_thesis: a "/\" bot = bot
hence  a "/\" bot = bot ; ::_thesis: verum
end;
then A11: OpenClosedSetLatt T is lower-bounded by LATTICES:def_13;
A12: OpenClosedSetLatt T is upper-bounded by A9, LATTICES:def_14;
A13: {} T = Bottom (OpenClosedSetLatt T) by A10, A11, LATTICES:def_16;
A14: [#] T = Top (OpenClosedSetLatt T) by A9, A12, LATTICES:def_17;
thus  OpenClosedSetLatt T is bounded by A11, A12; :: according to LATTICES:def_20 ::_thesis: ( OpenClosedSetLatt T is complemented & OpenClosedSetLatt T is distributive )
reconsider OCL = OpenClosedSetLatt T as 01_Lattice by A11, A12;
 for b being Element of OCL ex a being Element of OCL st a is_a_complement_of b
proof
let b be Element of OCL; ::_thesis: ex a being Element of OCL st a is_a_complement_of b
reconsider c = b as Element of OpenClosedSet T ;
reconsider a = c ` as Element of OCL by Th8;
A15: a "\/" b = c \/ (c `) by Def2
.= Top OCL by A14, PRE_TOPC:2 ;
A16: c misses c ` by XBOOLE_1:79;
A17: a "/\" b = c /\ (c `) by Def3
.= Bottom OCL by A13, A16, XBOOLE_0:def_7 ;
take  a ; ::_thesis: a is_a_complement_of b
thus  a is_a_complement_of b by A15, A17, LATTICES:def_18; ::_thesis: verum
end;
hence  ( OpenClosedSetLatt T is complemented & OpenClosedSetLatt T is distributive ) by A1, LATTICES:def_11, LATTICES:def_19; ::_thesis: verum
end;
end;

theorem :: LOPCLSET:13
for T being non empty TopSpace holds [#] T is Element of (OpenClosedSetLatt T) by Th3;

theorem :: LOPCLSET:14
for T being non empty TopSpace holds {} T is Element of (OpenClosedSetLatt T) by Th3;


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 bounded complemented Boolean for LattStr ;
existence
 not for b1 being B_Lattice holds b1 is trivial
proof
set T = the non empty TopSpace;
reconsider E = OpenClosedSetLatt the non empty TopSpace as B_Lattice ;
reconsider a = [#] the non empty TopSpace, b = {} the non empty TopSpace as Element of E by Th3;
take  E ; ::_thesis: not E is trivial
take  a ; :: according to STRUCT_0:def_10 ::_thesis: not for b1 being Element of the carrier of E holds a = b1
take  b ; ::_thesis: not a = b
thus  not a = b ; ::_thesis: verum
end;
end;


definition
let BL be non trivial B_Lattice;
func ultraset BL ->  Subset-Family of BL equals :: LOPCLSET:def 5
 {  F where F is Filter of BL : F is being_ultrafilter  }  ;
coherence
  {  F where F is Filter of BL : F is being_ultrafilter  }  is Subset-Family of BL
proof
set US =  {  F where F is Filter of BL : F is being_ultrafilter  }  ;
  {  F where F is Filter of BL : F is being_ultrafilter  }  c= bool the carrier of BL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F where F is Filter of BL : F is being_ultrafilter  }  or x in bool the carrier of BL )
assume  x in  {  F where F is Filter of BL : F is being_ultrafilter  }  ; ::_thesis: x in bool the carrier of BL
then  ex UF being Filter of BL st
( UF = x & UF is being_ultrafilter ) ;
hence  x in bool the carrier of BL ; ::_thesis: verum
end;
hence   {  F where F is Filter of BL : F is being_ultrafilter  }  is Subset-Family of BL ; ::_thesis: verum
end;
end;

:: deftheorem  defines ultraset LOPCLSET:def_5_:_
 for BL being non trivial B_Lattice holds ultraset BL =  {  F where F is Filter of BL : F is being_ultrafilter  }  ;

registration
let BL be non trivial B_Lattice;
cluster ultraset BL ->  non empty ;
coherence
 not ultraset BL is empty
proof
set US =  {  F where F is Filter of BL : F is being_ultrafilter  }  ;
consider p1, p2 being Element of BL such that
A1: p1 <> p2 by STRUCT_0:def_10;
 ( p1 <> Bottom BL or p2 <> Bottom BL ) by A1;
then consider p being Element of BL such that
A2: p <> Bottom BL ;
consider H being Filter of BL such that
 p in H and
A3: H is being_ultrafilter by A2, FILTER_0:20;
 H in  {  F where F is Filter of BL : F is being_ultrafilter  }  by A3;
hence  not ultraset BL is empty ; ::_thesis: verum
end;
end;

theorem :: LOPCLSET:15
for x being set
for BL being non trivial B_Lattice holds
( x in ultraset BL iff ex UF being Filter of BL st
( UF = x & UF is being_ultrafilter ) ) ;

theorem Th16: :: LOPCLSET:16
for BL being non trivial B_Lattice
for a being Element of BL holds  {  F where F is Filter of BL : ( F is being_ultrafilter & a in F )  }  c= ultraset BL
proof
let BL be non trivial B_Lattice; ::_thesis: for a being Element of BL holds  {  F where F is Filter of BL : ( F is being_ultrafilter & a in F )  }  c= ultraset BL
let a be Element of BL; ::_thesis:  {  F where F is Filter of BL : ( F is being_ultrafilter & a in F )  }  c= ultraset BL
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F where F is Filter of BL : ( F is being_ultrafilter & a in F )  }  or x in ultraset BL )
assume  x in  {  F where F is Filter of BL : ( F is being_ultrafilter & a in F )  }  ; ::_thesis: x in ultraset BL
then  ex UF being Filter of BL st
( UF = x & UF is being_ultrafilter & a in UF ) ;
hence  x in ultraset BL ; ::_thesis: verum
end;

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

:: deftheorem Def6 defines UFilter LOPCLSET:def_6_:_
 for BL being non trivial B_Lattice
for b2 being Function holds
( b2 = UFilter BL iff ( dom b2 = the carrier of BL & ( for a being Element of BL holds b2 . a =  {  UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF )  }  ) ) );

theorem Th17: :: LOPCLSET:17
for x being set
for BL being non trivial B_Lattice
for a being Element of BL holds
( x in (UFilter BL) . a iff ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) )
proof
let x be set ; ::_thesis: for BL being non trivial B_Lattice
for a being Element of BL holds
( x in (UFilter BL) . a iff ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) )
let BL be non trivial B_Lattice; ::_thesis: for a being Element of BL holds
( x in (UFilter BL) . a iff ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) )
let a be Element of BL; ::_thesis: ( x in (UFilter BL) . a iff ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) )
A1: ( x in (UFilter BL) . a implies ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) )
proof
assume  x in (UFilter BL) . a ; ::_thesis: ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F )
then  x in  {  UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF )  }  by Def6;
then consider F being Filter of BL such that
A2: F = x and
A3: F is being_ultrafilter and
A4: a in F ;
take  F ; ::_thesis: ( F = x & F is being_ultrafilter & a in F )
thus  ( F = x & F is being_ultrafilter & a in F ) by A2, A3, A4; ::_thesis: verum
end;
 ( ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) implies x in (UFilter BL) . a )
proof
assume  ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) ; ::_thesis: x in (UFilter BL) . a
then  x in  {  UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF )  }  ;
hence  x in (UFilter BL) . a by Def6; ::_thesis: verum
end;
hence  ( x in (UFilter BL) . a iff ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) ) by A1; ::_thesis: verum
end;

theorem Th18: :: LOPCLSET:18
for BL being non trivial B_Lattice
for a being Element of BL
for F being Filter of BL holds
( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )
proof
let BL be non trivial B_Lattice; ::_thesis: for a being Element of BL
for F being Filter of BL holds
( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )
let a be Element of BL; ::_thesis: for F being Filter of BL holds
( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )
let F be Filter of BL; ::_thesis: ( F in (UFilter BL) . a iff ( F is being_ultrafilter & a in F ) )
hereby  ::_thesis: ( F is being_ultrafilter & a in F implies F in (UFilter BL) . a )
assume  F in (UFilter BL) . a ; ::_thesis: ( F is being_ultrafilter & a in F )
then  ex F0 being Filter of BL st
( F0 = F & F0 is being_ultrafilter & a in F0 ) by Th17;
hence  ( F is being_ultrafilter & a in F ) ; ::_thesis: verum
end;
thus  ( F is being_ultrafilter & a in F implies F in (UFilter BL) . a ) by Th17; ::_thesis: verum
end;

theorem Th19: :: LOPCLSET:19
for BL being non trivial B_Lattice
for a, b being Element of BL
for F being Filter of BL st F is being_ultrafilter holds
( a "\/" b in F iff ( a in F or b in F ) )
proof
let BL be non trivial B_Lattice; ::_thesis: for a, b being Element of BL
for F being Filter of BL st F is being_ultrafilter holds
( a "\/" b in F iff ( a in F or b in F ) )
let a, b be Element of BL; ::_thesis: for F being Filter of BL st F is being_ultrafilter holds
( a "\/" b in F iff ( a in F or b in F ) )
let F be Filter of BL; ::_thesis: ( F is being_ultrafilter implies ( a "\/" b in F iff ( a in F or b in F ) ) )
assume  F is being_ultrafilter ; ::_thesis: ( a "\/" b in F iff ( a in F or b in F ) )
then  F is prime by FILTER_0:45;
hence  ( a "\/" b in F iff ( a in F or b in F ) ) by FILTER_0:def_5; ::_thesis: verum
end;

theorem Th20: :: LOPCLSET:20
for BL being non trivial B_Lattice
for a, b being Element of BL holds (UFilter BL) . (a "/\" b) = ((UFilter BL) . a) /\ ((UFilter BL) . b)
proof
let BL be non trivial B_Lattice; ::_thesis: for a, b being Element of BL holds (UFilter BL) . (a "/\" b) = ((UFilter BL) . a) /\ ((UFilter BL) . b)
let a, b be Element of BL; ::_thesis: (UFilter BL) . (a "/\" b) = ((UFilter BL) . a) /\ ((UFilter BL) . b)
A1: (UFilter BL) . (a "/\" b) c= ((UFilter BL) . a) /\ ((UFilter BL) . b)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (UFilter BL) . (a "/\" b) or x in ((UFilter BL) . a) /\ ((UFilter BL) . b) )
set c = a "/\" b;
assume  x in (UFilter BL) . (a "/\" b) ; ::_thesis: x in ((UFilter BL) . a) /\ ((UFilter BL) . b)
then consider F0 being Filter of BL such that
A2: x = F0 and
A3: F0 is being_ultrafilter and
A4: a "/\" b in F0 by Th17;
A5: a in F0 by A4, FILTER_0:8;
A6: b in F0 by A4, FILTER_0:8;
A7: F0 in (UFilter BL) . a by A3, A5, Th17;
 F0 in (UFilter BL) . b by A3, A6, Th17;
hence  x in ((UFilter BL) . a) /\ ((UFilter BL) . b) by A2, A7, XBOOLE_0:def_4; ::_thesis: verum
end;
 ((UFilter BL) . a) /\ ((UFilter BL) . b) c= (UFilter BL) . (a "/\" b)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((UFilter BL) . a) /\ ((UFilter BL) . b) or x in (UFilter BL) . (a "/\" b) )
assume A8: x in ((UFilter BL) . a) /\ ((UFilter BL) . b) ; ::_thesis: x in (UFilter BL) . (a "/\" b)
then A9: x in (UFilter BL) . a by XBOOLE_0:def_4;
A10: x in (UFilter BL) . b by A8, XBOOLE_0:def_4;
A11: ex F0 being Filter of BL st
( x = F0 & F0 is being_ultrafilter & a in F0 ) by A9, Th17;
 ex F0 being Filter of BL st
( x = F0 & F0 is being_ultrafilter & b in F0 ) by A10, Th17;
then consider F0 being Filter of BL such that
A12: x = F0 and
A13: F0 is being_ultrafilter and
A14: a in F0 and
A15: b in F0 by A11;
 a "/\" b in F0 by A14, A15, FILTER_0:8;
hence  x in (UFilter BL) . (a "/\" b) by A12, A13, Th17; ::_thesis: verum
end;
hence  (UFilter BL) . (a "/\" b) = ((UFilter BL) . a) /\ ((UFilter BL) . b) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th21: :: LOPCLSET:21
for BL being non trivial B_Lattice
for a, b being Element of BL holds (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b)
proof
let BL be non trivial B_Lattice; ::_thesis: for a, b being Element of BL holds (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b)
let a, b be Element of BL; ::_thesis: (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b)
A1: (UFilter BL) . (a "\/" b) c= ((UFilter BL) . a) \/ ((UFilter BL) . b)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (UFilter BL) . (a "\/" b) or x in ((UFilter BL) . a) \/ ((UFilter BL) . b) )
set c = a "\/" b;
assume  x in (UFilter BL) . (a "\/" b) ; ::_thesis: x in ((UFilter BL) . a) \/ ((UFilter BL) . b)
then consider F0 being Filter of BL such that
A2: x = F0 and
A3: F0 is being_ultrafilter and
A4: a "\/" b in F0 by Th17;
 ( a in F0 or b in F0 ) by A3, A4, Th19;
then  ( F0 in (UFilter BL) . a or F0 in (UFilter BL) . b ) by A3, Th17;
hence  x in ((UFilter BL) . a) \/ ((UFilter BL) . b) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
 ((UFilter BL) . a) \/ ((UFilter BL) . b) c= (UFilter BL) . (a "\/" b)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((UFilter BL) . a) \/ ((UFilter BL) . b) or x in (UFilter BL) . (a "\/" b) )
assume  x in ((UFilter BL) . a) \/ ((UFilter BL) . b) ; ::_thesis: x in (UFilter BL) . (a "\/" b)
then  ( x in (UFilter BL) . a or x in (UFilter BL) . b ) by XBOOLE_0:def_3;
then  ( ex F0 being Filter of BL st
( x = F0 & F0 is being_ultrafilter & a in F0 ) or ex F0 being Filter of BL st
( x = F0 & F0 is being_ultrafilter & b in F0 ) ) by Th17;
then consider F0 being Filter of BL such that
A5: x = F0 and
A6: F0 is being_ultrafilter and
A7: ( a in F0 or b in F0 ) ;
 a "\/" b in F0 by A6, A7, Th19;
hence  x in (UFilter BL) . (a "\/" b) by A5, A6, Th17; ::_thesis: verum
end;
hence  (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let BL be non trivial B_Lattice;
:: original: UFilter
redefine func UFilter BL ->  Function of the carrier of BL,(bool (ultraset BL));
coherence
 UFilter BL is Function of the carrier of BL,(bool (ultraset BL))
proof
reconsider f = UFilter BL as Function ;
A1: dom f = the carrier of BL by Def6;
 rng f c= bool (ultraset BL)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in bool (ultraset BL) )
assume  y in rng f ; ::_thesis: y in bool (ultraset BL)
then consider x being set  such that
A2: x in dom f and
A3: y = f . x by FUNCT_1:def_3;
 y =  {  F where F is Filter of BL : ( F is being_ultrafilter & x in F )  }  by A1, A2, A3, Def6;
then  y c= ultraset BL by A1, A2, Th16;
hence  y in bool (ultraset BL) ; ::_thesis: verum
end;
then reconsider f = f as Function of the carrier of BL,(bool (ultraset BL)) by A1, FUNCT_2:def_1, RELSET_1:4;
 for a being Element of BL holds f . a =  {  F where F is Filter of BL : ( F is being_ultrafilter & a in F )  }  by Def6;
hence  UFilter BL is Function of the carrier of BL,(bool (ultraset BL)) ; ::_thesis: verum
end;
end;

definition
let BL be non trivial B_Lattice;
func StoneR BL ->  set  equals :: LOPCLSET:def 7
 rng (UFilter BL);
coherence
 rng (UFilter BL) is set ;
end;

:: deftheorem  defines StoneR LOPCLSET:def_7_:_
 for BL being non trivial B_Lattice holds StoneR BL = rng (UFilter BL);

registration
let BL be non trivial B_Lattice;
cluster StoneR BL ->  non empty ;
coherence
 not StoneR BL is empty ;
end;

theorem :: LOPCLSET:22
for BL being non trivial B_Lattice holds StoneR BL c= bool (ultraset BL) ;

theorem Th23: :: LOPCLSET:23
for x being set
for BL being non trivial B_Lattice holds
( x in StoneR BL iff ex a being Element of BL st (UFilter BL) . a = x )
proof
let x be set ; ::_thesis: for BL being non trivial B_Lattice holds
( x in StoneR BL iff ex a being Element of BL st (UFilter BL) . a = x )
let BL be non trivial B_Lattice; ::_thesis: ( x in StoneR BL iff ex a being Element of BL st (UFilter BL) . a = x )
A1: ( x in StoneR BL implies ex a being Element of BL st (UFilter BL) . a = x )
proof
assume  x in StoneR BL ; ::_thesis: ex a being Element of BL st (UFilter BL) . a = x
then consider y being set  such that
A2: y in dom (UFilter BL) and
A3: x = (UFilter BL) . y by FUNCT_1:def_3;
reconsider a = y as Element of BL by A2;
take  a ; ::_thesis: (UFilter BL) . a = x
thus  (UFilter BL) . a = x by A3; ::_thesis: verum
end;
 ( ex a being Element of BL st (UFilter BL) . a = x implies x in StoneR BL )
proof
given a being Element of BL such that A4: x = (UFilter BL) . a ; ::_thesis: x in StoneR BL
 a in the carrier of BL ;
then  a in dom (UFilter BL) by Def6;
hence  x in StoneR BL by A4, FUNCT_1:def_3; ::_thesis: verum
end;
hence  ( x in StoneR BL iff ex a being Element of BL st (UFilter BL) . a = x ) by A1; ::_thesis: verum
end;

definition
let BL be non trivial B_Lattice;
func StoneSpace BL ->  strict TopSpace means :Def8: :: LOPCLSET:def 8
( the carrier of it = ultraset BL & the topology of it =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  );
existence
 ex b1 being strict TopSpace st
( the carrier of b1 = ultraset BL & the topology of b1 =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  )
proof
set US = ultraset BL;
set STP =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  ;
  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  c= bool (ultraset BL)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  or x in bool (ultraset BL) )
assume  x in  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  ; ::_thesis: x in bool (ultraset BL)
then  ex B being Subset-Family of (ultraset BL) st
( x = union B & B c= StoneR BL ) ;
hence  x in bool (ultraset BL) ; ::_thesis: verum
end;
then reconsider STP =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  as Subset-Family of (ultraset BL) ;
 TopStruct(# (ultraset BL),STP #) is strict TopSpace
proof
set TS = TopStruct(# (ultraset BL),STP #);
A1: the carrier of TopStruct(# (ultraset BL),STP #) in the topology of TopStruct(# (ultraset BL),STP #)
proof
set B =  {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  ;
  {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  c= ultraset BL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  or x in ultraset BL )
assume  x in  {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  ; ::_thesis: x in ultraset BL
then  ex F being Filter of BL st
( F = x & F is being_ultrafilter & Top BL in F ) ;
hence  x in ultraset BL ; ::_thesis: verum
end;
then A2: bool  {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  c= bool (ultraset BL) by ZFMISC_1:67;
 { {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  } c= bool  {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  by ZFMISC_1:68;
then reconsider SB = { {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  } as Subset-Family of (ultraset BL) by A2, XBOOLE_1:1;
reconsider SB = SB as Subset-Family of (ultraset BL) ;
A3: union SB =  {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  by ZFMISC_1:25;
 ultraset BL c=  {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ultraset BL or x in  {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  )
assume  x in ultraset BL ; ::_thesis: x in  {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }
then consider F being Filter of BL such that
A4: F = x and
A5: F is being_ultrafilter ;
 Top BL in F by FILTER_0:11;
hence  x in  {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  by A4, A5; ::_thesis: verum
end;
then A6: ultraset BL = union SB by A3, XBOOLE_0:def_10;
 (UFilter BL) . (Top BL) =  {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  by Def6;
then   {  F where F is Filter of BL : ( F is being_ultrafilter & Top BL in F )  }  in StoneR BL by Th23;
then  SB c= StoneR BL by ZFMISC_1:31;
hence  the carrier of TopStruct(# (ultraset BL),STP #) in the topology of TopStruct(# (ultraset BL),STP #) by A6; ::_thesis: verum
end;
A7: for a being Subset-Family of TopStruct(# (ultraset BL),STP #) st a c= the topology of TopStruct(# (ultraset BL),STP #) holds
union a in the topology of TopStruct(# (ultraset BL),STP #)
proof
let a be Subset-Family of TopStruct(# (ultraset BL),STP #); ::_thesis: ( a c= the topology of TopStruct(# (ultraset BL),STP #) implies union a in the topology of TopStruct(# (ultraset BL),STP #) )
assume A8: a c= the topology of TopStruct(# (ultraset BL),STP #) ; ::_thesis: union a in the topology of TopStruct(# (ultraset BL),STP #)
set B =  {  A where A is Subset of (StoneR BL) : union A in a  }  ;
  {  A where A is Subset of (StoneR BL) : union A in a  }  c= bool (StoneR BL)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  A where A is Subset of (StoneR BL) : union A in a  }  or x in bool (StoneR BL) )
assume  x in  {  A where A is Subset of (StoneR BL) : union A in a  }  ; ::_thesis: x in bool (StoneR BL)
then  ex C being Subset of (StoneR BL) st
( C = x & union C in a ) ;
then reconsider C = x as Subset of (StoneR BL) ;
 C c= StoneR BL ;
hence  x in bool (StoneR BL) ; ::_thesis: verum
end;
then reconsider BS =  {  A where A is Subset of (StoneR BL) : union A in a  }  as Subset-Family of (StoneR BL) ;
A9: union (union BS) = union  {  (union A) where A is Subset of (StoneR BL) : A in BS  }  by EQREL_1:54;
A10: a c=  {  (union A) where A is Subset of (StoneR BL) : A in BS  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a or x in  {  (union A) where A is Subset of (StoneR BL) : A in BS  }  )
assume A11: x in a ; ::_thesis: x in  {  (union A) where A is Subset of (StoneR BL) : A in BS  }
then  x in STP by A8;
then consider C being Subset-Family of (ultraset BL) such that
A12: x = union C and
A13: C c= StoneR BL ;
 C in BS by A11, A12, A13;
hence  x in  {  (union A) where A is Subset of (StoneR BL) : A in BS  }  by A12; ::_thesis: verum
end;
  {  (union A) where A is Subset of (StoneR BL) : A in BS  }  c= a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (union A) where A is Subset of (StoneR BL) : A in BS  }  or x in a )
assume  x in  {  (union A) where A is Subset of (StoneR BL) : A in BS  }  ; ::_thesis: x in a
then consider C being Subset of (StoneR BL) such that
A14: union C = x and
A15: C in BS ;
 ex D being Subset of (StoneR BL) st
( D = C & union D in a ) by A15;
hence  x in a by A14; ::_thesis: verum
end;
then A16: a =  {  (union A) where A is Subset of (StoneR BL) : A in BS  }  by A10, XBOOLE_0:def_10;
 union BS is Subset-Family of (ultraset BL) by XBOOLE_1:1;
hence  union a in the topology of TopStruct(# (ultraset BL),STP #) by A9, A16; ::_thesis: verum
end;
 for p, q being Subset of TopStruct(# (ultraset BL),STP #) st p in the topology of TopStruct(# (ultraset BL),STP #) & q in the topology of TopStruct(# (ultraset BL),STP #) holds
p /\ q in the topology of TopStruct(# (ultraset BL),STP #)
proof
let p, q be Subset of TopStruct(# (ultraset BL),STP #); ::_thesis: ( p in the topology of TopStruct(# (ultraset BL),STP #) & q in the topology of TopStruct(# (ultraset BL),STP #) implies p /\ q in the topology of TopStruct(# (ultraset BL),STP #) )
assume that
A17: p in the topology of TopStruct(# (ultraset BL),STP #) and
A18: q in the topology of TopStruct(# (ultraset BL),STP #) ; ::_thesis: p /\ q in the topology of TopStruct(# (ultraset BL),STP #)
consider P being Subset-Family of (ultraset BL) such that
A19: union P = p and
A20: P c= StoneR BL by A17;
consider Q being Subset-Family of (ultraset BL) such that
A21: union Q = q and
A22: Q c= StoneR BL by A18;
A23: (union P) /\ (union Q) = union (INTERSECTION (P,Q)) by SETFAM_1:28;
 INTERSECTION (P,Q) c= bool (ultraset BL)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in INTERSECTION (P,Q) or x in bool (ultraset BL) )
assume  x in INTERSECTION (P,Q) ; ::_thesis: x in bool (ultraset BL)
then consider X, Y being set  such that
A24: X in P and
A25: Y in Q and
A26: x = X /\ Y by SETFAM_1:def_5;
A27: X /\ Y c= X \/ Y by XBOOLE_1:29;
 X \/ Y c= ultraset BL by A24, A25, XBOOLE_1:8;
then  X /\ Y c= ultraset BL by A27, XBOOLE_1:1;
hence  x in bool (ultraset BL) by A26; ::_thesis: verum
end;
then reconsider C = INTERSECTION (P,Q) as Subset-Family of (ultraset BL) ;
reconsider C = C as Subset-Family of (ultraset BL) ;
 C c= StoneR BL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in StoneR BL )
assume  x in C ; ::_thesis: x in StoneR BL
then consider X, Y being set  such that
A28: X in P and
A29: Y in Q and
A30: x = X /\ Y by SETFAM_1:def_5;
consider a being Element of BL such that
A31: X = (UFilter BL) . a by A20, A28, Th23;
consider b being Element of BL such that
A32: Y = (UFilter BL) . b by A22, A29, Th23;
A33: X =  {  F where F is Filter of BL : ( F is being_ultrafilter & a in F )  }  by A31, Def6;
A34: Y =  {  F where F is Filter of BL : ( F is being_ultrafilter & b in F )  }  by A32, Def6;
A35: X /\ Y =  {  F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F )  }
proof
A36: X /\ Y c=  {  F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ Y or x in  {  F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F )  }  )
assume A37: x in X /\ Y ; ::_thesis: x in  {  F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F )  }
then A38: x in X by XBOOLE_0:def_4;
A39: x in Y by A37, XBOOLE_0:def_4;
consider F1 being Filter of BL such that
A40: x = F1 and
A41: F1 is being_ultrafilter and
A42: a in F1 by A33, A38;
 ex F2 being Filter of BL st
( x = F2 & F2 is being_ultrafilter & b in F2 ) by A34, A39;
then  a "/\" b in F1 by A40, A42, FILTER_0:8;
hence  x in  {  F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F )  }  by A40, A41; ::_thesis: verum
end;
  {  F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F )  }  c= X /\ Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F )  }  or x in X /\ Y )
assume  x in  {  F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F )  }  ; ::_thesis: x in X /\ Y
then consider F0 being Filter of BL such that
A43: x = F0 and
A44: F0 is being_ultrafilter and
A45: a "/\" b in F0 ;
 a in F0 by A45, FILTER_0:8;
then consider F being Filter of BL such that
A46: F = F0 and
A47: F is being_ultrafilter and
A48: a in F by A44;
A49: F in X by A33, A47, A48;
 b in F0 by A45, FILTER_0:8;
then consider F1 being Filter of BL such that
A50: F1 = F0 and
A51: F1 is being_ultrafilter and
A52: b in F1 by A44;
 F1 in Y by A34, A51, A52;
hence  x in X /\ Y by A43, A46, A49, A50, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  X /\ Y =  {  F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F )  }  by A36, XBOOLE_0:def_10; ::_thesis: verum
end;
 (UFilter BL) . (a "/\" b) =  {  F where F is Filter of BL : ( F is being_ultrafilter & a "/\" b in F )  }  by Def6;
hence  x in StoneR BL by A30, A35, Th23; ::_thesis: verum
end;
hence  p /\ q in the topology of TopStruct(# (ultraset BL),STP #) by A19, A21, A23; ::_thesis: verum
end;
hence  TopStruct(# (ultraset BL),STP #) is strict TopSpace by A1, A7, PRE_TOPC:def_1; ::_thesis: verum
end;
then reconsider TS = TopStruct(# (ultraset BL),STP #) as strict TopSpace ;
take  TS ; ::_thesis: ( the carrier of TS = ultraset BL & the topology of TS =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  )
thus  ( the carrier of TS = ultraset BL & the topology of TS =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict TopSpace st the carrier of b1 = ultraset BL & the topology of b1 =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  & the carrier of b2 = ultraset BL & the topology of b2 =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  holds
b1 = b2 ;
end;

:: deftheorem Def8 defines StoneSpace LOPCLSET:def_8_:_
 for BL being non trivial B_Lattice
for b2 being strict TopSpace holds
( b2 = StoneSpace BL iff ( the carrier of b2 = ultraset BL & the topology of b2 =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  ) );

registration
let BL be non trivial B_Lattice;
cluster StoneSpace BL ->  non empty strict ;
coherence
 not StoneSpace BL is empty
proof
 the carrier of (StoneSpace BL) = ultraset BL by Def8;
hence  not the carrier of (StoneSpace BL) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

theorem :: LOPCLSET:24
for BL being non trivial B_Lattice
for a being Element of BL
for F being Filter of BL st F is being_ultrafilter & not F in (UFilter BL) . a holds
not a in F by Th18;

theorem Th25: :: LOPCLSET:25
for BL being non trivial B_Lattice
for a being Element of BL holds (ultraset BL) \ ((UFilter BL) . a) = (UFilter BL) . (a `)
proof
let BL be non trivial B_Lattice; ::_thesis: for a being Element of BL holds (ultraset BL) \ ((UFilter BL) . a) = (UFilter BL) . (a `)
let a be Element of BL; ::_thesis: (ultraset BL) \ ((UFilter BL) . a) = (UFilter BL) . (a `)
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (UFilter BL) . (a `) c= (ultraset BL) \ ((UFilter BL) . a)
let x be set ; ::_thesis: ( x in (ultraset BL) \ ((UFilter BL) . a) implies x in (UFilter BL) . (a `) )
assume A1: x in (ultraset BL) \ ((UFilter BL) . a) ; ::_thesis: x in (UFilter BL) . (a `)
then A2: x in ultraset BL by XBOOLE_0:def_5;
A3: not x in (UFilter BL) . a by A1, XBOOLE_0:def_5;
consider F being Filter of BL such that
A4: F = x and
A5: F is being_ultrafilter by A2;
 not a in F by A3, A4, A5, Th18;
then  a ` in F by A5, FILTER_0:46;
hence  x in (UFilter BL) . (a `) by A4, A5, Th18; ::_thesis: verum
end;
hereby  :: according to TARSKI:def_3 ::_thesis: verum
let x be set ; ::_thesis: ( x in (UFilter BL) . (a `) implies x in (ultraset BL) \ ((UFilter BL) . a) )
assume  x in (UFilter BL) . (a `) ; ::_thesis: x in (ultraset BL) \ ((UFilter BL) . a)
then consider F being Filter of BL such that
A6: F = x and
A7: F is being_ultrafilter and
A8: a ` in F by Th17;
A9: not a in F by A7, A8, FILTER_0:46;
A10: F in ultraset BL by A7;
 not F in (UFilter BL) . a by A9, Th18;
hence  x in (ultraset BL) \ ((UFilter BL) . a) by A6, A10, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

definition
let BL be non trivial B_Lattice;
func StoneBLattice BL ->  Lattice equals :: LOPCLSET:def 9
 OpenClosedSetLatt (StoneSpace BL);
coherence
 OpenClosedSetLatt (StoneSpace BL) is Lattice ;
end;

:: deftheorem  defines StoneBLattice LOPCLSET:def_9_:_
 for BL being non trivial B_Lattice holds StoneBLattice BL = OpenClosedSetLatt (StoneSpace BL);

Lm1:  for BL being non trivial B_Lattice
for p being Subset of (StoneSpace BL) st p in StoneR BL holds
p is open
proof
let BL be non trivial B_Lattice; ::_thesis: for p being Subset of (StoneSpace BL) st p in StoneR BL holds
p is open
let p be Subset of (StoneSpace BL); ::_thesis: ( p in StoneR BL implies p is open )
assume A1: p in StoneR BL ; ::_thesis: p is open
then A2: {p} is Subset-Family of (ultraset BL) by SUBSET_1:41;
A3: {p} c= StoneR BL by A1, ZFMISC_1:31;
 union {p} = p by ZFMISC_1:25;
then  p in  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  by A2, A3;
then  p in the topology of (StoneSpace BL) by Def8;
hence  p is open by PRE_TOPC:def_2; ::_thesis: verum
end;

registration
let BL be non trivial B_Lattice;
cluster UFilter BL ->  one-to-one ;
coherence
 UFilter BL is one-to-one
proof
now__::_thesis:_for_a,_b_being_Element_of_BL_st_(UFilter_BL)_._a_=_(UFilter_BL)_._b_holds_
a_=_b
let a, b be Element of BL; ::_thesis: ( (UFilter BL) . a = (UFilter BL) . b implies a = b )
assume A1: (UFilter BL) . a = (UFilter BL) . b ; ::_thesis: a = b
assume  not a = b ; ::_thesis: contradiction
then consider UF being Filter of BL such that
A2: UF is being_ultrafilter and
A3: ( ( a in UF & not b in UF ) or ( not a in UF & b in UF ) ) by FILTER_0:47;
now__::_thesis:_(_(_a_in_UF_&_not_b_in_UF_&_(UFilter_BL)_._a_<>_(UFilter_BL)_._b_)_or_(_not_a_in_UF_&_b_in_UF_&_(UFilter_BL)_._a_<>_(UFilter_BL)_._b_)_)
percases ( ( a in UF & not b in UF ) or ( not a in UF & b in UF ) ) by A3;
caseA4: ( a in UF & not b in UF ) ; ::_thesis: (UFilter BL) . a <> (UFilter BL) . b
then  UF in (UFilter BL) . a by A2, Th18;
hence  (UFilter BL) . a <> (UFilter BL) . b by A4, Th18; ::_thesis: verum
end;
case ( not a in UF & b in UF ) ; ::_thesis: (UFilter BL) . a <> (UFilter BL) . b
then  not UF in (UFilter BL) . a by Th18;
hence  (UFilter BL) . a <> (UFilter BL) . b by A2, A3, Th18; ::_thesis: verum
end;
end;
end;
hence  contradiction by A1; ::_thesis: verum
end;
hence  UFilter BL is one-to-one by GROUP_6:1; ::_thesis: verum
end;
end;

theorem :: LOPCLSET:26
for BL being non trivial B_Lattice holds union (StoneR BL) = ultraset BL
proof
let BL be non trivial B_Lattice; ::_thesis: union (StoneR BL) = ultraset BL
set x = the Element of OpenClosedSet (StoneSpace BL);
reconsider X = the Element of OpenClosedSet (StoneSpace BL) as Subset of (StoneSpace BL) ;
A1: X is open by Th1;
A2: X is closed by Th2;
 X in the topology of (StoneSpace BL) by A1, PRE_TOPC:def_2;
then  X in  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  by Def8;
then consider B being Subset-Family of (ultraset BL) such that
A3: union B = X and
A4: B c= StoneR BL ;
 X ` is open by A2;
then  X ` in the topology of (StoneSpace BL) by PRE_TOPC:def_2;
then  X ` in  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  by Def8;
then consider C being Subset-Family of (ultraset BL) such that
A5: union C = X ` and
A6: C c= StoneR BL ;
 B \/ C c= StoneR BL by A4, A6, XBOOLE_1:8;
then  union (B \/ C) c= union (StoneR BL) by ZFMISC_1:77;
then  X \/ (X `) c= union (StoneR BL) by A3, A5, ZFMISC_1:78;
then  [#] (StoneSpace BL) c= union (StoneR BL) by PRE_TOPC:2;
then A7: ultraset BL c= union (StoneR BL) by Def8;
 union (StoneR BL) c= union (bool (ultraset BL)) by ZFMISC_1:77;
then  union (StoneR BL) c= ultraset BL by ZFMISC_1:81;
hence  union (StoneR BL) = ultraset BL by A7, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th27: :: LOPCLSET:27
for X being non empty set holds
not for Y being Finite_Subset of X holds Y is empty
proof
let X be non empty set ; ::_thesis: not for Y being Finite_Subset of X holds Y is empty
set a = the Element of X;
 {. the Element of X.} is Finite_Subset of X ;
hence  not for Y being Finite_Subset of X holds Y is empty ; ::_thesis: verum
end;

registration
let D be non empty set ;
cluster non empty finite for Element of Fin D;
existence
 not for b1 being Finite_Subset of D holds b1 is empty by Th27;
end;

theorem Th28: :: LOPCLSET:28
for L being non trivial B_Lattice
for D being non empty Subset of L st Bottom L in <.D.) holds
ex B being non empty Finite_Subset of the carrier of L st
( B c= D & FinMeet B = Bottom L )
proof
let L be non trivial B_Lattice; ::_thesis: for D being non empty Subset of L st Bottom L in <.D.) holds
ex B being non empty Finite_Subset of the carrier of L st
( B c= D & FinMeet B = Bottom L )
let D be non empty Subset of L; ::_thesis: ( Bottom L in <.D.) implies ex B being non empty Finite_Subset of the carrier of L st
( B c= D & FinMeet B = Bottom L ) )
assume A1: Bottom L in <.D.) ; ::_thesis: ex B being non empty Finite_Subset of the carrier of L st
( B c= D & FinMeet B = Bottom L )
set A =  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  ;
set AA =  {  a where a is Element of L : ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= a )  }  ;
A2:  {  a where a is Element of L : ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= a )  }  c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  a where a is Element of L : ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= a )  }  or x in the carrier of L )
assume  x in  {  a where a is Element of L : ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= a )  }  ; ::_thesis: x in the carrier of L
then  ex a being Element of L st
( a = x & ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= a ) ) ;
hence  x in the carrier of L ; ::_thesis: verum
end;
 not  {  a where a is Element of L : ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= a )  }  is empty
proof
consider C being Finite_Subset of D such that
A3: not C is empty by Th27;
A4: C is Subset of D by FINSUB_1:17;
then  C c= the carrier of L by XBOOLE_1:1;
then  C is Element of Fin the carrier of L by FINSUB_1:def_5;
then consider C being Element of Fin the carrier of L such that
A5: C <> {} and
A6: C c= D by A3, A4;
reconsider a = FinMeet C as Element of L ;
 a in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  by A5, A6;
then  a in  {  a where a is Element of L : ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= a )  }  ;
hence  not  {  a where a is Element of L : ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= a )  }  is empty ; ::_thesis: verum
end;
then reconsider AA =  {  a where a is Element of L : ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= a )  }  as non empty Subset of L by A2;
A7: for p, q being Element of L st p in AA & q in AA holds
p "/\" q in AA
proof
let p, q be Element of L; ::_thesis: ( p in AA & q in AA implies p "/\" q in AA )
assume that
A8: p in AA and
A9: q in AA ; ::_thesis: p "/\" q in AA
consider a being Element of L such that
A10: a = p and
A11: ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= a ) by A8;
consider c being Element of L such that
A12: c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  and
A13: c [= a by A11;
consider b being Element of L such that
A14: b = q and
A15: ex d being Element of L st
( d in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & d [= b ) by A9;
consider d being Element of L such that
A16: d in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  and
A17: d [= b by A15;
A18: c "/\" d [= a "/\" b by A13, A17, FILTER_0:5;
consider C being Element of Fin the carrier of L such that
A19: c = FinMeet C and
A20: C c= D and
A21: C <> {} by A12;
consider E being Element of Fin the carrier of L such that
A22: d = FinMeet E and
A23: E c= D and
 E <> {} by A16;
A24: c "/\" d = FinMeet (C \/ E) by A19, A22, LATTICE4:23;
 C \/ E c= D by A20, A23, XBOOLE_1:8;
then  c "/\" d in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  by A21, A24;
hence  p "/\" q in AA by A10, A14, A18; ::_thesis: verum
end;
 for p, q being Element of L st p in AA & p [= q holds
q in AA
proof
let p, q be Element of L; ::_thesis: ( p in AA & p [= q implies q in AA )
assume that
A25: p in AA and
A26: p [= q ; ::_thesis: q in AA
A27: ex a being Element of L st
( a = p & ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= a ) ) by A25;
 ex b being Element of L st
( b = q & ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= b ) ) by A26, A27, LATTICES:7;
hence  q in AA ; ::_thesis: verum
end;
then A28: AA is Filter of L by A7, FILTER_0:9;
 D c= AA
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in AA )
assume A29: x in D ; ::_thesis: x in AA
then A30: {x} c= D by ZFMISC_1:31;
 {x} c= the carrier of L by A29, ZFMISC_1:31;
then reconsider C = {x} as Element of Fin the carrier of L by FINSUB_1:def_5;
A31: x = (id the carrier of L) . x by A29, FUNCT_1:18
.= the L_meet of L $$ (C,(id the carrier of L)) by A29, SETWISEO:17
.= FinMeet (C,(id L)) by LATTICE2:def_4
.= FinMeet C by LATTICE4:def_8 ;
reconsider a = FinMeet C as Element of L ;
 a in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  by A30;
hence  x in AA by A31; ::_thesis: verum
end;
then  <.D.) c= AA by A28, FILTER_0:def_4;
then  Bottom L in AA by A1;
then  ex d being Element of L st
( d = Bottom L & ex c being Element of L st
( c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  & c [= d ) ) ;
then consider c being Element of L such that
A32: c in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  and
A33: c [= Bottom L ;
 Bottom L [= c by LATTICES:16;
then  Bottom L in  {  (FinMeet C) where C is Element of Fin the carrier of L : ( C c= D & C <> {} )  }  by A32, A33, LATTICES:8;
then  ex C being Finite_Subset of the carrier of L st
( Bottom L = FinMeet C & C c= D & C <> {} ) ;
hence  ex B being non empty Finite_Subset of the carrier of L st
( B c= D & FinMeet B = Bottom L ) ; ::_thesis: verum
end;

theorem Th29: :: LOPCLSET:29
for L being 0_Lattice
for F being Filter of L holds
( not F is being_ultrafilter or not Bottom L in F )
proof
let L be 0_Lattice; ::_thesis: for F being Filter of L holds
( not F is being_ultrafilter or not Bottom L in F )
given F being Filter of L such that A1: F is being_ultrafilter and
A2: Bottom L in F ; ::_thesis: contradiction
 F = the carrier of L by A2, FILTER_0:26;
hence  contradiction by A1, FILTER_0:def_3; ::_thesis: verum
end;

theorem Th30: :: LOPCLSET:30
for BL being non trivial B_Lattice holds (UFilter BL) . (Bottom BL) = {}
proof
let BL be non trivial B_Lattice; ::_thesis: (UFilter BL) . (Bottom BL) = {}
assume A1: (UFilter BL) . (Bottom BL) <> {} ; ::_thesis: contradiction
set x = the Element of (UFilter BL) . (Bottom BL);
 ex F being Filter of BL st
( F = the Element of (UFilter BL) . (Bottom BL) & F is being_ultrafilter & Bottom BL in F ) by A1, Th17;
hence  contradiction by Th29; ::_thesis: verum
end;

theorem :: LOPCLSET:31
for BL being non trivial B_Lattice holds (UFilter BL) . (Top BL) = ultraset BL
proof
let BL be non trivial B_Lattice; ::_thesis: (UFilter BL) . (Top BL) = ultraset BL
thus (UFilter BL) . (Top BL) = (UFilter BL) . ((Bottom BL) `) by LATTICE4:30
.= (ultraset BL) \ ((UFilter BL) . (Bottom BL)) by Th25
.= (ultraset BL) \ {} by Th30
.= ultraset BL ; ::_thesis: verum
end;

theorem Th32: :: LOPCLSET:32
for X being set
for BL being non trivial B_Lattice st ultraset BL = union X & X is Subset of (StoneR BL) holds
ex Y being Finite_Subset of X st ultraset BL = union Y
proof
let X be set ; ::_thesis: for BL being non trivial B_Lattice st ultraset BL = union X & X is Subset of (StoneR BL) holds
ex Y being Finite_Subset of X st ultraset BL = union Y
let BL be non trivial B_Lattice; ::_thesis: ( ultraset BL = union X & X is Subset of (StoneR BL) implies ex Y being Finite_Subset of X st ultraset BL = union Y )
assume that
A1: ultraset BL = union X and
A2: X is Subset of (StoneR BL) ; ::_thesis: ex Y being Finite_Subset of X st ultraset BL = union Y
assume A3: for Y being Finite_Subset of X holds not ultraset BL = union Y ; ::_thesis: contradiction
consider Y being Finite_Subset of X such that
A4: not Y is empty by A1, Th27, ZFMISC_1:2;
A5: Y c= X by FINSUB_1:def_5;
then A6: Y c= StoneR BL by A2, XBOOLE_1:1;
set x = the Element of Y;
A7: the Element of Y in X by A4, A5, TARSKI:def_3;
 the Element of Y in StoneR BL by A4, A6, TARSKI:def_3;
then consider b being Element of BL such that
A8: the Element of Y = (UFilter BL) . b by Th23;
set CY =  {  (a `) where a is Element of BL : (UFilter BL) . a in X  }  ;
consider c being Element of BL such that
A9: c = b ` ;
A10: c in  {  (a `) where a is Element of BL : (UFilter BL) . a in X  }  by A7, A8, A9;
  {  (a `) where a is Element of BL : (UFilter BL) . a in X  }  c= the carrier of BL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (a `) where a is Element of BL : (UFilter BL) . a in X  }  or x in the carrier of BL )
assume  x in  {  (a `) where a is Element of BL : (UFilter BL) . a in X  }  ; ::_thesis: x in the carrier of BL
then  ex b being Element of BL st
( x = b ` & (UFilter BL) . b in X ) ;
hence  x in the carrier of BL ; ::_thesis: verum
end;
then reconsider CY =  {  (a `) where a is Element of BL : (UFilter BL) . a in X  }  as non empty Subset of BL by A10;
set H = <.CY.);
 for B being non empty Finite_Subset of the carrier of BL st B c= CY holds
FinMeet B <> Bottom BL
proof
let B be non empty Finite_Subset of the carrier of BL; ::_thesis: ( B c= CY implies FinMeet B <> Bottom BL )
assume that
A11: B c= CY and
A12: FinMeet B = Bottom BL ; ::_thesis: contradiction
A13: B is Subset of BL by FINSUB_1:17;
A14: dom (UFilter BL) = the carrier of BL by FUNCT_2:def_1;
 (UFilter BL) .: B c= rng (UFilter BL) by RELAT_1:111;
then reconsider D = (UFilter BL) .: B as non empty Subset-Family of (ultraset BL) by A13, A14, XBOOLE_1:1;
A15: now__::_thesis:_not_{}_(ultraset_BL)_<>_(UFilter_BL)_._(Bottom_BL)
set x = the Element of (UFilter BL) . (Bottom BL);
assume  {} (ultraset BL) <> (UFilter BL) . (Bottom BL) ; ::_thesis: contradiction
then  ex F being Filter of BL st
( F = the Element of (UFilter BL) . (Bottom BL) & F is being_ultrafilter & Bottom BL in F ) by Th17;
hence  contradiction by Th29; ::_thesis: verum
end;
deffunc H1( Subset of (ultraset BL), Subset of (ultraset BL)) ->  Element of K19((ultraset BL)) = $1 /\ $2;
consider G being BinOp of (bool (ultraset BL)) such that
A16: for x, y being Subset of (ultraset BL) holds G . (x,y) = H1(x,y) from BINOP_1:sch_4();
A17: G is commutative
proof
let x, y be Subset of (ultraset BL); :: according to BINOP_1:def_2 ::_thesis: G . (x,y) = G . (y,x)
G . (x,y) = y /\ x by A16
.= G . (y,x) by A16 ;
hence  G . (x,y) = G . (y,x) ; ::_thesis: verum
end;
A18: G is associative
proof
let x, y, z be Subset of (ultraset BL); :: according to BINOP_1:def_3 ::_thesis: G . (x,(G . (y,z))) = G . ((G . (x,y)),z)
G . (x,(G . (y,z))) = G . (x,(y /\ z)) by A16
.= x /\ (y /\ z) by A16
.= (x /\ y) /\ z by XBOOLE_1:16
.= G . ((x /\ y),z) by A16
.= G . ((G . (x,y)),z) by A16 ;
hence  G . (x,(G . (y,z))) = G . ((G . (x,y)),z) ; ::_thesis: verum
end;
A19: G is idempotent
proof
let x be Subset of (ultraset BL); :: according to BINOP_1:def_4 ::_thesis: G . (x,x) = x
G . (x,x) = x /\ x by A16
.= x ;
hence  G . (x,x) = x ; ::_thesis: verum
end;
A20: for x, y being Element of BL holds (UFilter BL) . ( the L_meet of BL . (x,y)) = G . (((UFilter BL) . x),((UFilter BL) . y))
proof
let x, y be Element of BL; ::_thesis: (UFilter BL) . ( the L_meet of BL . (x,y)) = G . (((UFilter BL) . x),((UFilter BL) . y))
thus (UFilter BL) . ( the L_meet of BL . (x,y)) = (UFilter BL) . (x "/\" y)
.= ((UFilter BL) . x) /\ ((UFilter BL) . y) by Th20
.= G . (((UFilter BL) . x),((UFilter BL) . y)) by A16 ; ::_thesis: verum
end;
reconsider DD = D as Element of Fin (bool (ultraset BL)) ;
 id BL = id the carrier of BL ;
then A21: (UFilter BL) . (FinMeet B) = (UFilter BL) . (FinMeet (B,(id the carrier of BL))) by LATTICE4:def_8
.= (UFilter BL) . ( the L_meet of BL $$ (B,(id the carrier of BL))) by LATTICE2:def_4
.= G $$ (B,((UFilter BL) * (id the carrier of BL))) by A17, A18, A19, A20, SETWISEO:30
.= G $$ (B,(UFilter BL)) by FUNCT_2:17
.= G $$ (B,((id (bool (ultraset BL))) * (UFilter BL))) by FUNCT_2:17
.= G $$ (DD,(id (bool (ultraset BL)))) by A17, A18, A19, SETWISEO:29 ;
defpred S1[ Element of Fin (bool (ultraset BL))] means  for D being non empty Subset-Family of (ultraset BL) st D = $1 holds
G $$ ($1,(id (bool (ultraset BL)))) = meet D;
A22: S1[ {}. (bool (ultraset BL))] ;
A23: for DD being Element of Fin (bool (ultraset BL))
for b being Subset of (ultraset BL) st S1[DD] holds
S1[DD \/ {.b.}]
proof
let DD be Element of Fin (bool (ultraset BL)); ::_thesis: for b being Subset of (ultraset BL) st S1[DD] holds
S1[DD \/ {.b.}]
let b be Subset of (ultraset BL); ::_thesis: ( S1[DD] implies S1[DD \/ {.b.}] )
assume A24: for D being non empty Subset-Family of (ultraset BL) st D = DD holds
G $$ (DD,(id (bool (ultraset BL)))) = meet D ; ::_thesis: S1[DD \/ {.b.}]
let D be non empty Subset-Family of (ultraset BL); ::_thesis: ( D = DD \/ {.b.} implies G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D )
assume A25: D = DD \/ {b} ; ::_thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D
now__::_thesis:_G_$$_((DD_\/_{.b.}),(id_(bool_(ultraset_BL))))_=_meet_D
percases ( DD is empty or not DD is empty ) ;
supposeA26: DD is empty ; ::_thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D
hence G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = (id (bool (ultraset BL))) . b by A17, A18, SETWISEO:17
.= b by FUNCT_1:18
.= meet D by A25, A26, SETFAM_1:10 ;
::_thesis: verum
end;
supposeA27: not DD is empty ; ::_thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D
 DD c= D by A25, XBOOLE_1:7;
then reconsider D1 = DD as non empty Subset-Family of (ultraset BL) by A27, XBOOLE_1:1;
reconsider D1 = D1 as non empty Subset-Family of (ultraset BL) ;
thus G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = G . ((G $$ (DD,(id (bool (ultraset BL))))),((id (bool (ultraset BL))) . b)) by A17, A18, A19, A27, SETWISEO:20
.= G . ((G $$ (DD,(id (bool (ultraset BL))))),b) by FUNCT_1:18
.= (G $$ (DD,(id (bool (ultraset BL))))) /\ b by A16
.= (meet D1) /\ b by A24
.= (meet D1) /\ (meet {b}) by SETFAM_1:10
.= meet D by A25, SETFAM_1:9 ; ::_thesis: verum
end;
end;
end;
hence  G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = meet D ; ::_thesis: verum
end;
 for DD being Element of Fin (bool (ultraset BL)) holds S1[DD] from SETWISEO:sch_4(A22, A23);
then  meet D = {} (ultraset BL) by A12, A15, A21;
then A28: union (COMPLEMENT D) = ([#] (ultraset BL)) \ {} by SETFAM_1:34
.= ultraset BL ;
A29: COMPLEMENT D c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in COMPLEMENT D or x in X )
assume A30: x in COMPLEMENT D ; ::_thesis: x in X
then reconsider c = x as Subset of (ultraset BL) ;
 c ` in D by A30, SETFAM_1:def_7;
then consider a being set  such that
A31: a in dom (UFilter BL) and
A32: a in B and
A33: c ` = (UFilter BL) . a by FUNCT_1:def_6;
reconsider a = a as Element of BL by A31;
 a in CY by A11, A32;
then  (a `) ` in CY ;
then consider b being Element of BL such that
A34: b ` = (a `) ` and
A35: (UFilter BL) . b in X ;
x = ((UFilter BL) . a) ` by A33
.= (UFilter BL) . (a `) by Th25
.= (UFilter BL) . ((b `) `) by A34
.= (UFilter BL) . b ;
hence  x in X by A35; ::_thesis: verum
end;
 COMPLEMENT D is finite
proof
A36: D is finite ;
deffunc H2( Subset of (ultraset BL)) ->  Element of K19((ultraset BL)) = $1 ` ;
A37:  {  H2(w) where w is Subset of (ultraset BL) : w in D  }  is finite from FRAENKEL:sch_21(A36);
  {  (w `) where w is Subset of (ultraset BL) : w in D  }  = COMPLEMENT D
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: COMPLEMENT D c=  {  (w `) where w is Subset of (ultraset BL) : w in D  }
let x be set ; ::_thesis: ( x in  {  (w `) where w is Subset of (ultraset BL) : w in D  }  implies x in COMPLEMENT D )
assume  x in  {  (w `) where w is Subset of (ultraset BL) : w in D  }  ; ::_thesis: x in COMPLEMENT D
then consider w being Subset of (ultraset BL) such that
A38: w ` = x and
A39: w in D ;
 (w `) ` in D by A39;
hence  x in COMPLEMENT D by A38, SETFAM_1:def_7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in COMPLEMENT D or x in  {  (w `) where w is Subset of (ultraset BL) : w in D  }  )
assume A40: x in COMPLEMENT D ; ::_thesis: x in  {  (w `) where w is Subset of (ultraset BL) : w in D  }
then reconsider x9 = x as Subset of (ultraset BL) ;
A41: x9 ` in D by A40, SETFAM_1:def_7;
 (x9 `) ` = x9 ;
hence  x in  {  (w `) where w is Subset of (ultraset BL) : w in D  }  by A41; ::_thesis: verum
end;
hence  COMPLEMENT D is finite by A37; ::_thesis: verum
end;
then  COMPLEMENT D is Finite_Subset of X by A29, FINSUB_1:def_5;
hence  contradiction by A3, A28; ::_thesis: verum
end;
then  <.CY.) <> the carrier of BL by Th28;
then consider F being Filter of BL such that
A42: <.CY.) c= F and
A43: F is being_ultrafilter by FILTER_0:18;
A44: CY c= <.CY.) by FILTER_0:def_4;
 not F in union X
proof
assume  F in union X ; ::_thesis: contradiction
then consider Y being set  such that
A45: F in Y and
A46: Y in X by TARSKI:def_4;
consider a being set  such that
A47: a in dom (UFilter BL) and
A48: Y = (UFilter BL) . a by A2, A46, FUNCT_1:def_3;
reconsider a = a as Element of BL by A47;
 a ` in CY by A46, A48;
then A49: a ` in <.CY.) by A44;
 a in F by A45, A48, Th18;
hence  contradiction by A42, A43, A49, FILTER_0:46; ::_thesis: verum
end;
hence  contradiction by A1, A43; ::_thesis: verum
end;

Lm2:  for BL being non trivial B_Lattice holds StoneR BL c= OpenClosedSet (StoneSpace BL)
proof
let BL be non trivial B_Lattice; ::_thesis: StoneR BL c= OpenClosedSet (StoneSpace BL)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in StoneR BL or x in OpenClosedSet (StoneSpace BL) )
assume A1: x in StoneR BL ; ::_thesis: x in OpenClosedSet (StoneSpace BL)
then reconsider p = x as Subset of (StoneSpace BL) by Def8;
A2: p is open by A1, Lm1;
 p is closed
proof
set ST = StoneSpace BL;
A3: [#] (StoneSpace BL) = ultraset BL by Def8;
consider a being Element of BL such that
A4: (UFilter BL) . a = p by A1, Th23;
 p ` = (UFilter BL) . (a `) by A3, A4, Th25;
then  p ` in StoneR BL by Th23;
then  p ` is open by Lm1;
hence  p is closed by TOPS_1:3; ::_thesis: verum
end;
hence  x in OpenClosedSet (StoneSpace BL) by A2; ::_thesis: verum
end;

theorem Th33: :: LOPCLSET:33
for BL being non trivial B_Lattice holds StoneR BL = OpenClosedSet (StoneSpace BL)
proof
let BL be non trivial B_Lattice; ::_thesis: StoneR BL = OpenClosedSet (StoneSpace BL)
A1: StoneR BL c= OpenClosedSet (StoneSpace BL) by Lm2;
 OpenClosedSet (StoneSpace BL) c= StoneR BL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OpenClosedSet (StoneSpace BL) or x in StoneR BL )
assume A2: x in OpenClosedSet (StoneSpace BL) ; ::_thesis: x in StoneR BL
then reconsider X = x as Subset of (StoneSpace BL) ;
A3: the topology of (StoneSpace BL) =  {  (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL  }  by Def8;
A4: ( X is open & X is closed ) by A2, Th1, Th2;
then A5: ( X ` is open & X ` is closed ) ;
 X in the topology of (StoneSpace BL) by A4, PRE_TOPC:def_2;
then consider A1 being Subset-Family of (ultraset BL) such that
A6: X = union A1 and
A7: A1 c= StoneR BL by A3;
 X ` in the topology of (StoneSpace BL) by A5, PRE_TOPC:def_2;
then consider A2 being Subset-Family of (ultraset BL) such that
A8: X ` = union A2 and
A9: A2 c= StoneR BL by A3;
A10: X is Subset of (ultraset BL) by Def8;
set AA = A1 \/ A2;
A11: ultraset BL = [#] (StoneSpace BL) by Def8
.= X \/ (X `) by PRE_TOPC:2
.= union (A1 \/ A2) by A6, A8, ZFMISC_1:78 ;
A12: A1 \/ A2 c= StoneR BL by A7, A9, XBOOLE_1:8;
then consider Y being Finite_Subset of (A1 \/ A2) such that
A13: ultraset BL = union Y by A11, Th32;
A14: Y c= A1 \/ A2 by FINSUB_1:def_5;
then A15: Y c= StoneR BL by A12, XBOOLE_1:1;
set D = A1 /\ Y;
A16: Y = (A1 \/ A2) /\ Y by A14, XBOOLE_1:28
.= (A1 /\ Y) \/ (A2 /\ Y) by XBOOLE_1:23 ;
now__::_thesis:_for_y_being_set_st_y_in_A2_/\_Y_holds_
y_misses_X
let y be set ; ::_thesis: ( y in A2 /\ Y implies y misses X )
assume  y in A2 /\ Y ; ::_thesis: y misses X
then  y in A2 by XBOOLE_0:def_4;
then A17: y c= X ` by A8, ZFMISC_1:74;
 X ` misses X by XBOOLE_1:79;
then  (X `) /\ X = {} by XBOOLE_0:def_7;
then  y /\ X = {} by A17, XBOOLE_1:3, XBOOLE_1:26;
hence  y misses X by XBOOLE_0:def_7; ::_thesis: verum
end;
then A18: X c= union (A1 /\ Y) by A10, A13, A16, SETFAM_1:42;
percases ( A1 /\ Y = {} or A1 /\ Y <> {} ) ;
suppose A1 /\ Y = {} ; ::_thesis: x in StoneR BL
then A19: X = {} by A18, ZFMISC_1:2;
 {} = (UFilter BL) . (Bottom BL) by Th30;
hence  x in StoneR BL by A19, FUNCT_2:4; ::_thesis: verum
end;
supposeA20: A1 /\ Y <> {} ; ::_thesis: x in StoneR BL
A21: A1 /\ Y c= Y by XBOOLE_1:17;
reconsider D = A1 /\ Y as non empty Subset-Family of (ultraset BL) by A20;
reconsider D = D as non empty Subset-Family of (ultraset BL) ;
A22: union D c= (union A1) /\ (union Y) by ZFMISC_1:79;
 (union A1) /\ (union Y) c= union A1 by XBOOLE_1:17;
then  union D c= X by A6, A22, XBOOLE_1:1;
then A23: X = union D by A18, XBOOLE_0:def_10;
A24: D c= rng (UFilter BL) by A15, A21, XBOOLE_1:1;
A25: rng (UFilter BL) = dom (id (StoneR BL)) ;
A26: dom (UFilter BL) = dom (UFilter BL) ;
 UFilter BL = (id (StoneR BL)) * (UFilter BL) by RELAT_1:54;
then  UFilter BL, id (StoneR BL) are_fiberwise_equipotent by A25, A26, CLASSES1:77;
then  card ((UFilter BL) " D) = card ((id (StoneR BL)) " D) by CLASSES1:78
.= card D by A24, FUNCT_2:94 ;
then  (UFilter BL) " D is finite ;
then reconsider B = (UFilter BL) " D as Finite_Subset of the carrier of BL by FINSUB_1:def_5;
A27: D = (UFilter BL) .: B by A15, A21, FUNCT_1:77, XBOOLE_1:1;
then A28: not B is empty ;
deffunc H1( Subset of (ultraset BL), Subset of (ultraset BL)) ->  Element of K19((ultraset BL)) = $1 \/ $2;
consider G being BinOp of (bool (ultraset BL)) such that
A29: for x, y being Subset of (ultraset BL) holds G . (x,y) = H1(x,y) from BINOP_1:sch_4();
A30: G is commutative
proof
let x, y be Subset of (ultraset BL); :: according to BINOP_1:def_2 ::_thesis: G . (x,y) = G . (y,x)
G . (x,y) = y \/ x by A29
.= G . (y,x) by A29 ;
hence  G . (x,y) = G . (y,x) ; ::_thesis: verum
end;
A31: G is associative
proof
let x, y, z be Subset of (ultraset BL); :: according to BINOP_1:def_3 ::_thesis: G . (x,(G . (y,z))) = G . ((G . (x,y)),z)
G . (x,(G . (y,z))) = G . (x,(y \/ z)) by A29
.= x \/ (y \/ z) by A29
.= (x \/ y) \/ z by XBOOLE_1:4
.= G . ((x \/ y),z) by A29
.= G . ((G . (x,y)),z) by A29 ;
hence  G . (x,(G . (y,z))) = G . ((G . (x,y)),z) ; ::_thesis: verum
end;
A32: G is idempotent
proof
let x be Subset of (ultraset BL); :: according to BINOP_1:def_4 ::_thesis: G . (x,x) = x
G . (x,x) = x \/ x by A29
.= x ;
hence  G . (x,x) = x ; ::_thesis: verum
end;
A33: for x, y being Element of BL holds (UFilter BL) . ( the L_join of BL . (x,y)) = G . (((UFilter BL) . x),((UFilter BL) . y))
proof
let x, y be Element of BL; ::_thesis: (UFilter BL) . ( the L_join of BL . (x,y)) = G . (((UFilter BL) . x),((UFilter BL) . y))
thus (UFilter BL) . ( the L_join of BL . (x,y)) = (UFilter BL) . (x "\/" y)
.= ((UFilter BL) . x) \/ ((UFilter BL) . y) by Th21
.= G . (((UFilter BL) . x),((UFilter BL) . y)) by A29 ; ::_thesis: verum
end;
reconsider DD = D as Element of Fin (bool (ultraset BL)) by FINSUB_1:def_5;
 id BL = id the carrier of BL ;
then A34: (UFilter BL) . (FinJoin B) = (UFilter BL) . (FinJoin (B,(id the carrier of BL))) by LATTICE4:def_7
.= (UFilter BL) . ( the L_join of BL $$ (B,(id the carrier of BL))) by LATTICE2:def_3
.= G $$ (B,((UFilter BL) * (id the carrier of BL))) by A28, A30, A31, A32, A33, SETWISEO:30
.= G $$ (B,(UFilter BL)) by FUNCT_2:17
.= G $$ (B,((id (bool (ultraset BL))) * (UFilter BL))) by FUNCT_2:17
.= G $$ (DD,(id (bool (ultraset BL)))) by A27, A28, A30, A31, A32, SETWISEO:29 ;
defpred S1[ Element of Fin (bool (ultraset BL))] means  for D being non empty Subset-Family of (ultraset BL) st D = $1 holds
G $$ ($1,(id (bool (ultraset BL)))) = union D;
A35: S1[ {}. (bool (ultraset BL))] ;
A36: for DD being Element of Fin (bool (ultraset BL))
for b being Subset of (ultraset BL) st S1[DD] holds
S1[DD \/ {.b.}]
proof
let DD be Element of Fin (bool (ultraset BL)); ::_thesis: for b being Subset of (ultraset BL) st S1[DD] holds
S1[DD \/ {.b.}]
let b be Subset of (ultraset BL); ::_thesis: ( S1[DD] implies S1[DD \/ {.b.}] )
assume A37: for D being non empty Subset-Family of (ultraset BL) st D = DD holds
G $$ (DD,(id (bool (ultraset BL)))) = union D ; ::_thesis: S1[DD \/ {.b.}]
let D be non empty Subset-Family of (ultraset BL); ::_thesis: ( D = DD \/ {.b.} implies G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union D )
assume A38: D = DD \/ {b} ; ::_thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union D
now__::_thesis:_G_$$_((DD_\/_{.b.}),(id_(bool_(ultraset_BL))))_=_union_D
percases ( DD is empty or not DD is empty ) ;
supposeA39: DD is empty ; ::_thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union D
hence G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = (id (bool (ultraset BL))) . b by A30, A31, SETWISEO:17
.= b by FUNCT_1:18
.= union D by A38, A39, ZFMISC_1:25 ;
::_thesis: verum
end;
supposeA40: not DD is empty ; ::_thesis: G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union D
 DD c= D by A38, XBOOLE_1:7;
then reconsider D1 = DD as non empty Subset-Family of (ultraset BL) by A40, XBOOLE_1:1;
reconsider D1 = D1 as non empty Subset-Family of (ultraset BL) ;
thus G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = G . ((G $$ (DD,(id (bool (ultraset BL))))),((id (bool (ultraset BL))) . b)) by A30, A31, A32, A40, SETWISEO:20
.= G . ((G $$ (DD,(id (bool (ultraset BL))))),b) by FUNCT_1:18
.= (G $$ (DD,(id (bool (ultraset BL))))) \/ b by A29
.= (union D1) \/ b by A37
.= (union D1) \/ (union {b}) by ZFMISC_1:25
.= union D by A38, ZFMISC_1:78 ; ::_thesis: verum
end;
end;
end;
hence  G $$ ((DD \/ {.b.}),(id (bool (ultraset BL)))) = union D ; ::_thesis: verum
end;
 for DD being Element of Fin (bool (ultraset BL)) holds S1[DD] from SETWISEO:sch_4(A35, A36);
then  (UFilter BL) . (FinJoin B) = x by A23, A34;
hence  x in StoneR BL by FUNCT_2:4; ::_thesis: verum
end;
end;
end;
hence  StoneR BL = OpenClosedSet (StoneSpace BL) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let BL be non trivial B_Lattice;
:: original: UFilter
redefine func UFilter BL ->  Homomorphism of BL, StoneBLattice BL;
coherence
 UFilter BL is Homomorphism of BL, StoneBLattice BL
proof
reconsider g = UFilter BL as Function of the carrier of BL,(bool (ultraset BL)) ;
set SL = StoneBLattice BL;
 rng g = StoneR BL ;
then  rng g c= OpenClosedSet (StoneSpace BL) by Lm2;
then reconsider f = UFilter BL as Function of the carrier of BL, the carrier of (StoneBLattice BL) by FUNCT_2:6;
now__::_thesis:_for_p,_q_being_Element_of_BL_holds_
(_f_._(p_"\/"_q)_=_(f_._p)_"\/"_(f_._q)_&_f_._(p_"/\"_q)_=_(f_._p)_"/\"_(f_._q)_)
let p, q be Element of BL; ::_thesis: ( f . (p "\/" q) = (f . p) "\/" (f . q) & f . (p "/\" q) = (f . p) "/\" (f . q) )
thus f . (p "\/" q) = (f . p) \/ (f . q) by Th21
.= (f . p) "\/" (f . q) by Def2 ; ::_thesis: f . (p "/\" q) = (f . p) "/\" (f . q)
thus f . (p "/\" q) = (f . p) /\ (f . q) by Th20
.= (f . p) "/\" (f . q) by Def3 ; ::_thesis: verum
end;
hence  UFilter BL is Homomorphism of BL, StoneBLattice BL by LATTICE4:def_1; ::_thesis: verum
end;
end;

theorem Th34: :: LOPCLSET:34
for BL being non trivial B_Lattice holds rng (UFilter BL) = the carrier of (StoneBLattice BL)
proof
let BL be non trivial B_Lattice; ::_thesis: rng (UFilter BL) = the carrier of (StoneBLattice BL)
thus  rng (UFilter BL) = StoneR BL
.= the carrier of (StoneBLattice BL) by Th33 ; ::_thesis: verum
end;

registration
let BL be non trivial B_Lattice;
cluster UFilter BL ->  bijective for Function of BL,(StoneBLattice BL);
coherence
 for b1 being Function of BL,(StoneBLattice BL) st b1 = UFilter BL holds
b1 is bijective
proof
 rng (UFilter BL) = the carrier of (StoneBLattice BL) by Th34;
then  UFilter BL is onto by FUNCT_2:def_3;
hence  for b1 being Function of BL,(StoneBLattice BL) st b1 = UFilter BL holds
b1 is bijective ; ::_thesis: verum
end;
end;

theorem Th35: :: LOPCLSET:35
for BL being non trivial B_Lattice holds BL, StoneBLattice BL are_isomorphic
proof
let BL be non trivial B_Lattice; ::_thesis: BL, StoneBLattice BL are_isomorphic
 ex f being Homomorphism of BL, StoneBLattice BL st
( f = UFilter BL & f is bijective ) ;
hence  BL, StoneBLattice BL are_isomorphic by LATTICE4:def_2; ::_thesis: verum
end;

theorem :: LOPCLSET:36
for BL being non trivial B_Lattice ex T being non empty TopSpace st BL, OpenClosedSetLatt T are_isomorphic
proof
let BL be non trivial B_Lattice; ::_thesis: ex T being non empty TopSpace st BL, OpenClosedSetLatt T are_isomorphic
reconsider T = StoneSpace BL as non empty TopSpace ;
take  T ; ::_thesis: BL, OpenClosedSetLatt T are_isomorphic
 OpenClosedSetLatt T = StoneBLattice BL ;
hence  BL, OpenClosedSetLatt T are_isomorphic by Th35; ::_thesis: verum
end;