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)

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

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

then reconsider top = { (union A) where A is Subset of (StoneS H) : verum } as Subset-Family of (F_primeSet H) ;
let x be object ; :: 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) )

reconsider xx = x as set by TARSKI:1;

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;

then xx 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;reconsider xx = x as set by TARSKI:1;

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;

then xx 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

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