let X, Y be non empty TopSpace; :: thesis: for D being Subset of [:X,Y:] st D is open holds
for X1 being Subset of X
for Y1 being Subset of Y holds
( ( X1 = (pr1 the carrier of X,the carrier of Y) .: D implies X1 is open ) & ( Y1 = (pr2 the carrier of X,the carrier of Y) .: D implies Y1 is open ) )
let D be Subset of [:X,Y:]; :: thesis: ( D is open implies for X1 being Subset of X
for Y1 being Subset of Y holds
( ( X1 = (pr1 the carrier of X,the carrier of Y) .: D implies X1 is open ) & ( Y1 = (pr2 the carrier of X,the carrier of Y) .: D implies Y1 is open ) ) )
set p = pr2 the carrier of X,the carrier of Y;
set P = .: (pr2 the carrier of X,the carrier of Y);
assume D is open ; :: thesis: for X1 being Subset of X
for Y1 being Subset of Y holds
( ( X1 = (pr1 the carrier of X,the carrier of Y) .: D implies X1 is open ) & ( Y1 = (pr2 the carrier of X,the carrier of Y) .: D implies Y1 is open ) )
then consider H being Subset-Family of [:X,Y:] such that
A1: D = union H and
A2: for e being set st e in H holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by Th45;
reconsider K = H as Subset-Family of [:the carrier of X,the carrier of Y:] by Def5;
let X1 be Subset of X; :: thesis: for Y1 being Subset of Y holds
( ( X1 = (pr1 the carrier of X,the carrier of Y) .: D implies X1 is open ) & ( Y1 = (pr2 the carrier of X,the carrier of Y) .: D implies Y1 is open ) )
let Y1 be Subset of Y; :: thesis: ( ( X1 = (pr1 the carrier of X,the carrier of Y) .: D implies X1 is open ) & ( Y1 = (pr2 the carrier of X,the carrier of Y) .: D implies Y1 is open ) )
A3: {} X = {} ;
thus ( X1 = (pr1 the carrier of X,the carrier of Y) .: D implies X1 is open ) :: thesis: ( Y1 = (pr2 the carrier of X,the carrier of Y) .: D implies Y1 is open )

proof

set p = pr1 the carrier of X,the carrier of Y;
set P = .: (pr1 the carrier of X,the carrier of Y);
reconsider PK = (.: (pr1 the carrier of X,the carrier of Y)) .: K as Subset-Family of X ;
reconsider PK = PK as Subset-Family of X ;
A4: PK is open

proof

let X1 be Subset of X; :: according to TOPS_2:def 1 :: thesis: ( not X1 in PK or X1 is open )
reconsider x1 = X1 as Subset of X ;
assume X1 in PK ; :: thesis: X1 is open
then consider c being Subset of [:the carrier of X,the carrier of Y:] such that
A5: c in K and
A6: x1 = (.: (pr1 the carrier of X,the carrier of Y)) . c by FUNCT_2:116;
dom (.: (pr1 the carrier of X,the carrier of Y)) = bool [:the carrier of X,the carrier of Y:] by FUNCT_2:def 1;
then A7: X1 = (pr1 the carrier of X,the carrier of Y) .: c by A6, FUNCT_3:8;
A8: ( c = {} or c <> {} ) ;
ex X2 being Subset of X ex Y2 being Subset of Y st
( c = [:X2,Y2:] & X2 is open & Y2 is open ) by A2, A5;
hence X1 is open by A3, A7, A8, EQREL_1:58, RELAT_1:149; :: thesis: verum

end;

assume X1 = (pr1 the carrier of X,the carrier of Y) .: D ; :: thesis: X1 is open
then X1 = union ((.: (pr1 the carrier of X,the carrier of Y)) .: K) by A1, EQREL_1:62;
hence X1 is open by A4, TOPS_2:26; :: thesis: verum

end;

reconsider PK = (.: (pr2 the carrier of X,the carrier of Y)) .: K as Subset-Family of Y ;
reconsider PK = PK as Subset-Family of Y ;
A9: {} Y = {} ;
A10: PK is open

proof

let Y1 be Subset of Y; :: according to TOPS_2:def 1 :: thesis: ( not Y1 in PK or Y1 is open )
reconsider y1 = Y1 as Subset of Y ;
assume Y1 in PK ; :: thesis: Y1 is open
then consider c being Subset of [:the carrier of X,the carrier of Y:] such that
A11: c in K and
A12: y1 = (.: (pr2 the carrier of X,the carrier of Y)) . c by FUNCT_2:116;
dom (.: (pr2 the carrier of X,the carrier of Y)) = bool [:the carrier of X,the carrier of Y:] by FUNCT_2:def 1;
then A13: Y1 = (pr2 the carrier of X,the carrier of Y) .: c by A12, FUNCT_3:8;
A14: ( c = {} or c <> {} ) ;
ex X2 being Subset of X ex Y2 being Subset of Y st
( c = [:X2,Y2:] & X2 is open & Y2 is open ) by A2, A11;
hence Y1 is open by A9, A13, A14, EQREL_1:58, RELAT_1:149; :: thesis: verum

end;

assume Y1 = (pr2 the carrier of X,the carrier of Y) .: D ; :: thesis: Y1 is open
then Y1 = union ((.: (pr2 the carrier of X,the carrier of Y)) .: K) by A1, EQREL_1:62;
hence Y1 is open by A10, TOPS_2:26; :: thesis: verum