let X, Y be non empty TopSpace; :: thesis: 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:]; :: thesis: ( H is open implies ( (Pr1 X,Y) .: H is open & (Pr2 X,Y) .: H is open ) )
assume A1: H is open ; :: thesis: ( (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 ;
A2: P1 is open

proof

let X1 be Subset of X; :: according to TOPS_2:def 1 :: thesis: ( not X1 in P1 or X1 is open )
assume X1 in P1 ; :: thesis: X1 is open
then consider D being Subset of [:X,Y:] such that
A3: ( D in H & X1 = (pr1 the carrier of X,the carrier of Y) .: D ) by Th57;
D is open by A1, A3, TOPS_2:def 1;
hence X1 is open by A3, Th59; :: thesis: verum

end;

P2 is open

proof

let Y1 be Subset of Y; :: according to TOPS_2:def 1 :: thesis: ( not Y1 in P2 or Y1 is open )
assume Y1 in P2 ; :: thesis: Y1 is open
then consider D being Subset of [:X,Y:] such that
A4: ( D in H & Y1 = (pr2 the carrier of X,the carrier of Y) .: D ) by Th58;
D is open by A1, A4, TOPS_2:def 1;
hence Y1 is open by A4, Th59; :: thesis: verum

end;

hence ( (Pr1 X,Y) .: H is open & (Pr2 X,Y) .: H is open ) by A2; :: thesis: verum