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:] ;

hence [:V,W:] is open by A2, Th5; :: thesis: verum

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 )

[:V,W:] = union {[:V,W:]}
;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;( 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

hence [:V,W:] is open by A2, Th5; :: thesis: verum