let X, Y be non empty TopSpace; for H being Subset-Family of [:X,Y:] st H is open holds
( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open )
let H be Subset-Family of [:X,Y:]; ( H is open implies ( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open ) )
reconsider P1 = (Pr1 (X,Y)) .: H as Subset-Family of X ;
reconsider P2 = (Pr2 (X,Y)) .: H as Subset-Family of Y ;
assume A1:
H is open
; ( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open )
A2:
P2 is open
P1 is open
hence
( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open )
by A2; verum