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 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;

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