let X, Y be non empty TopSpace; :: thesis: for H being Subset-Family of st H is open holds
( (Pr1 X,Y) .: H is open & (Pr2 X,Y) .: H is open )
let H be Subset-Family of ; :: 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 ;
reconsider P2 = (Pr2 X,Y) .: H as Subset-Family of ;
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 ; :: 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 such that
A3: D in H and
A4: Y1 = (pr2 the carrier of X,the carrier of Y) .: D by Th58;
D is open by A1, A3, TOPS_2:def 1;
hence Y1 is open by A4, Th59; :: thesis: verum

end;

P1 is open

proof

let X1 be Subset of ; :: 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 such that
A5: D in H and
A6: X1 = (pr1 the carrier of X,the carrier of Y) .: D by Th57;
D is open by A1, A5, TOPS_2:def 1;
hence X1 is open by A6, Th59; :: thesis: verum

end;

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