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)) )
assume A1: x in StoneS H ; :: thesis: x in the carrier of (Open_setLatt (HTopSpace H))
set carrO = the carrier of (Open_setLatt (HTopSpace H));
A2: the carrier of (Open_setLatt (HTopSpace H)) = { (union A) where A is Subset of (StoneS H) : verum } by Def12;
reconsider z = {x} as Subset of (StoneS H) by A1, ZFMISC_1:37;
union z = x by ZFMISC_1:31;
hence x in the carrier of (Open_setLatt (HTopSpace H)) by A2; :: thesis: verum