let X, Y be TopSpace; :: thesis: for V being Subset of X
for W being Subset of Y st V is open & W is open holds
[:V,W:] is open
let V be Subset of X; :: thesis: for W being Subset of Y st V is open & W is open holds
[:V,W:] is open
let W be Subset of Y; :: 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 [:X,Y:] ;
reconsider PP = PP as Subset-Family of [:X,Y:] ;
A2: now :: thesis: for e being set st e in PP holds
ex V being Subset of X ex W being Subset of Y st
( e = [:V,W:] & V is open & W is open )
let e be set ; :: thesis: ( e in PP implies ex V being Subset of X ex W being Subset of Y st
( e = [:V,W:] & V is open & W is open ) )
assume A3: e in PP ; :: thesis: ex V being Subset of X ex W being Subset of Y st
( e = [:V,W:] & V is open & W is open )
take V = V; :: thesis: ex W being Subset of Y 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:]} ;
hence [:V,W:] is open by A2, Th5; :: thesis: verum