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

( (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

P1 is open
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;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

proof

hence
( (Pr1 (X,Y)) .: H is open & (Pr2 (X,Y)) .: H is open )
by A2; :: thesis: verum
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;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