reconsider A1 = {((StoneH H) . (Top H))} as Subset of (StoneS H) ;
set TS = HTopSpace H;
A1: the topology of (HTopSpace H) = { (union A) where A is Subset of (StoneS H) : verum } by Def12;
A2: the carrier of (HTopSpace H) = F_primeSet H by Def12;
hence not HTopSpace H is empty ; :: thesis: HTopSpace H is TopSpace-like
F_primeSet H = (StoneH H) . (Top H) by Th28;
then F_primeSet H = union A1 by ZFMISC_1:25;
hence the carrier of (HTopSpace H) in the topology of (HTopSpace H) by A2, A1; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b₁ being Element of K19(K19( the carrier of (HTopSpace H))) holds
( not b₁ c= the topology of (HTopSpace H) or union b₁ in the topology of (HTopSpace H) ) ) & ( for b₁, b₂ being Element of K19( the carrier of (HTopSpace H)) holds
( not b₁ in the topology of (HTopSpace H) or not b₂ in the topology of (HTopSpace H) or b₁ /\ b₂ in the topology of (HTopSpace H) ) ) )

hereby :: thesis: for b₁, b₂ being Element of K19( the carrier of (HTopSpace H)) holds
( not b₁ in the topology of (HTopSpace H) or not b₂ in the topology of (HTopSpace H) or b₁ /\ b₂ in the topology of (HTopSpace H) )

let a be Subset-Family of (HTopSpace H); :: thesis: ( a c= the topology of (HTopSpace H) implies union a in the topology of (HTopSpace H) )
defpred S₁[ set ] means union H in a;
set B = { A where A is Subset of (StoneS H) : S₁[A] } ;
set X = { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S₁[A] } } ;
assume A3: a c= the topology of (HTopSpace H) ; :: thesis: union a in the topology of (HTopSpace H)
A4: a = { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S₁[A] } }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S₁[A] } } c= a

let x be object ; :: thesis: ( x in a implies x in { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S₁[A] } } )
assume A5: x in a ; :: thesis: x in { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S₁[A] } }
then x in the topology of (HTopSpace H) by A3;
then consider A being Subset of (StoneS H) such that
A6: x = union A by A1;
A in { A where A is Subset of (StoneS H) : S₁[A] } by A5, A6;
hence x in { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S₁[A] } } by A6; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S₁[A] } } or x in a )
assume x in { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S₁[A] } } ; :: thesis: x in a
then consider A being Subset of (StoneS H) such that
A7: x = union A and
A8: A in { A where A is Subset of (StoneS H) : S₁[A] } ;
ex A9 being Subset of (StoneS H) st
( A = A9 & union A9 in a ) by A8;
hence x in a by A7; :: thesis: verum

end;

reconsider B = { A where A is Subset of (StoneS H) : S₁[A] } as Subset-Family of (StoneS H) from DOMAIN_1:sch 7();
union (union B) = union a by A4, EQREL_1:54;
hence union a in the topology of (HTopSpace H) by A1; :: thesis: verum

end;

let a, b be Subset of (HTopSpace H); :: thesis: ( not a in the topology of (HTopSpace H) or not b in the topology of (HTopSpace H) or a /\ b in the topology of (HTopSpace H) )
assume that
A9: a in the topology of (HTopSpace H) and
A10: b in the topology of (HTopSpace H) ; :: thesis: a /\ b in the topology of (HTopSpace H)
consider A being Subset of (StoneS H) such that
A11: a = union A by A1, A9;
consider B being Subset of (StoneS H) such that
A12: b = union B by A1, A10;
INTERSECTION (A,B) c= StoneS H

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in INTERSECTION (A,B) or x in StoneS H )
assume x in INTERSECTION (A,B) ; :: thesis: x in StoneS H
then consider X, Y being set such that
A13: X in A and
A14: Y in B and
A15: x = X /\ Y by SETFAM_1:def 5;
consider p9 being Element of H such that
A16: X = (StoneH H) . p9 by A13, Th13;
consider q9 being Element of H such that
A17: Y = (StoneH H) . q9 by A14, Th13;
x = (StoneH H) . (p9 "/\" q9) by A15, A16, A17, Th15;
hence x in StoneS H ; :: thesis: verum

end;

then reconsider C = INTERSECTION (A,B) as Subset of (StoneS H) ;
(union A) /\ (union B) = union C by SETFAM_1:28;
hence a /\ b in the topology of (HTopSpace H) by A1, A11, A12; :: thesis: verum