let H be non trivial H_Lattice; :: thesis: StoneS H c= the carrier of (Open_setLatt (HTopSpace H))
let x be object ; :: 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