let X, Y be TopSpace; :: thesis: for V being Subset of
for W being Subset of st V is open & W is open holds
[:V,W:] is open
let V be Subset of ; :: thesis: for W being Subset of st V is open & W is open holds
[:V,W:] is open
let W be Subset of ; :: thesis: ( V is open & W is open implies [:V,W:] is open )
assume A1: ( V is open & W is open ) ; :: thesis: [:V,W:] is open
reconsider PP = {[:V,W:]} as Subset-Family of ;
reconsider PP = PP as Subset-Family of ;

A2: now

let e be set ; :: thesis: ( e in PP implies ex V being Subset of ex W being Subset of st
( e = [:V,W:] & V is open & W is open ) )
assume A3: e in PP ; :: thesis: ex V being Subset of ex W being Subset of st
( e = [:V,W:] & V is open & W is open )
take V = V; :: thesis: ex W being Subset of st
( e = [:V,W:] & V is open & W is open )
take W = W; :: thesis: ( e = [:V,W:] & V is open & W is open )
thus ( e = [:V,W:] & V is open & W is open ) by A1, A3, TARSKI:def 1; :: thesis: verum

end;

[:V,W:] = union {[:V,W:]} by ZFMISC_1:31;
hence [:V,W:] is open by A2, Th45; :: thesis: verum