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 Th5;

reconsider K = H as Subset-Family of [: the carrier of X, the carrier of Y:] by Def2;

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

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 )

reconsider PK = PK as Subset-Family of Y ;

A8: PK is open

then Y1 = union ((.: (pr2 ( the carrier of X, the carrier of Y))) .: K) by A1, EQREL_1:53;

hence Y1 is open by A8, TOPS_2:19; :: thesis: verum

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 Th5;

reconsider K = H as Subset-Family of [: the carrier of X, the carrier of Y:] by Def2;

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

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

reconsider PK = (.: (pr2 ( the carrier of X, the carrier of Y))) .: K as Subset-Family of Y ;
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 ;

A3: PK is open

then X1 = union ((.: (pr1 ( the carrier of X, the carrier of Y))) .: K) by A1, EQREL_1:53;

hence X1 is open by A3, TOPS_2:19; :: thesis: verum

end;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 ;

A3: PK is open

proof

assume
X1 = (pr1 ( the carrier of X, the carrier of Y)) .: D
; :: thesis: X1 is open
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

A4: c in K and

A5: x1 = (.: (pr1 ( the carrier of X, the carrier of Y))) . c by FUNCT_2:65;

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 A6: X1 = (pr1 ( the carrier of X, the carrier of Y)) .: c by A5, FUNCT_3:7;

A7: ( 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, A4;

hence X1 is open by A6, A7, EQREL_1:49; :: thesis: verum

end;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

A4: c in K and

A5: x1 = (.: (pr1 ( the carrier of X, the carrier of Y))) . c by FUNCT_2:65;

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 A6: X1 = (pr1 ( the carrier of X, the carrier of Y)) .: c by A5, FUNCT_3:7;

A7: ( 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, A4;

hence X1 is open by A6, A7, EQREL_1:49; :: thesis: verum

then X1 = union ((.: (pr1 ( the carrier of X, the carrier of Y))) .: K) by A1, EQREL_1:53;

hence X1 is open by A3, TOPS_2:19; :: thesis: verum

reconsider PK = PK as Subset-Family of Y ;

A8: PK is open

proof

assume
Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: D
; :: thesis: Y1 is open
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

A9: c in K and

A10: y1 = (.: (pr2 ( the carrier of X, the carrier of Y))) . c by FUNCT_2:65;

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 A11: Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: c by A10, FUNCT_3:7;

A12: ( 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, A9;

hence Y1 is open by A11, A12, EQREL_1:49; :: thesis: verum

end;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

A9: c in K and

A10: y1 = (.: (pr2 ( the carrier of X, the carrier of Y))) . c by FUNCT_2:65;

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 A11: Y1 = (pr2 ( the carrier of X, the carrier of Y)) .: c by A10, FUNCT_3:7;

A12: ( 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, A9;

hence Y1 is open by A11, A12, EQREL_1:49; :: thesis: verum

then Y1 = union ((.: (pr2 ( the carrier of X, the carrier of Y))) .: K) by A1, EQREL_1:53;

hence Y1 is open by A8, TOPS_2:19; :: thesis: verum