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

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