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 ) )
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 ; :: thesis: ( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open )
A2: 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
A3: D in H and
A4: Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D by Th17;
D is open by A1, A3;
hence Y1 is open by A4, Th18; :: thesis: verum

end;

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
A5: D in H and
A6: X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D by Th16;
D is open by A1, A5;
hence X1 is open by A6, Th18; :: thesis: verum

end;

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