let X, Y be non empty TopSpace; :: thesis: for H being Subset-Family of [:X,Y:]

for X1 being Subset of X

for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds

( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )

let H be Subset-Family of [:X,Y:]; :: thesis: for X1 being Subset of X

for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds

( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )

let X1 be Subset of X; :: thesis: for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds

( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )

let Y1 be Subset of Y; :: thesis: ( H is Cover of [:X1,Y1:] implies ( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) ) )

A1: dom (.: (pr2 ( the carrier of X, the carrier of Y))) = bool (dom (pr2 ( the carrier of X, the carrier of Y))) by FUNCT_3:def 1

.= bool [: the carrier of X, the carrier of Y:] by FUNCT_3:def 5 ;

A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;

assume A3: [:X1,Y1:] c= union H ; :: according to SETFAM_1:def 11 :: thesis: ( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )

thus ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) :: thesis: ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 )

then consider x being Point of X such that

A11: x in X1 by SUBSET_1:4;

let e be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not e in Y1 or e in union ((Pr2 (X,Y)) .: H) )

assume A12: e in Y1 ; :: thesis: e in union ((Pr2 (X,Y)) .: H)

then reconsider y = e as Point of Y ;

[x,y] in [:X1,Y1:] by A11, A12, ZFMISC_1:87;

then consider A being set such that

A13: [x,y] in A and

A14: A in H by A3, TARSKI:def 4;

[x,y] in [: the carrier of X, the carrier of Y:] by ZFMISC_1:87;

then A15: [x,y] in dom (pr2 ( the carrier of X, the carrier of Y)) by FUNCT_3:def 5;

e = (pr2 ( the carrier of X, the carrier of Y)) . (x,y) by FUNCT_3:def 5;

then A16: e in (pr2 ( the carrier of X, the carrier of Y)) .: A by A13, A15, FUNCT_1:def 6;

(.: (pr2 ( the carrier of X, the carrier of Y))) . A = (pr2 ( the carrier of X, the carrier of Y)) .: A by A2, A14, EQREL_1:48;

then (pr2 ( the carrier of X, the carrier of Y)) .: A in (Pr2 (X,Y)) .: H by A2, A14, A1, FUNCT_1:def 6;

hence e in union ((Pr2 (X,Y)) .: H) by A16, TARSKI:def 4; :: thesis: verum

for X1 being Subset of X

for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds

( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )

let H be Subset-Family of [:X,Y:]; :: thesis: for X1 being Subset of X

for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds

( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )

let X1 be Subset of X; :: thesis: for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds

( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )

let Y1 be Subset of Y; :: thesis: ( H is Cover of [:X1,Y1:] implies ( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) ) )

A1: dom (.: (pr2 ( the carrier of X, the carrier of Y))) = bool (dom (pr2 ( the carrier of X, the carrier of Y))) by FUNCT_3:def 1

.= bool [: the carrier of X, the carrier of Y:] by FUNCT_3:def 5 ;

A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;

assume A3: [:X1,Y1:] c= union H ; :: according to SETFAM_1:def 11 :: thesis: ( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )

thus ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) :: thesis: ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 )

proof

assume
X1 <> {}
; :: thesis: (Pr2 (X,Y)) .: H is Cover of Y1
assume
Y1 <> {}
; :: thesis: (Pr1 (X,Y)) .: H is Cover of X1

then consider y being Point of Y such that

A4: y in Y1 by SUBSET_1:4;

let e be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not e in X1 or e in union ((Pr1 (X,Y)) .: H) )

assume A5: e in X1 ; :: thesis: e in union ((Pr1 (X,Y)) .: H)

then reconsider x = e as Point of X ;

[x,y] in [:X1,Y1:] by A4, A5, ZFMISC_1:87;

then consider A being set such that

A6: [x,y] in A and

A7: A in H by A3, TARSKI:def 4;

[x,y] in [: the carrier of X, the carrier of Y:] by ZFMISC_1:87;

then A8: [x,y] in dom (pr1 ( the carrier of X, the carrier of Y)) by FUNCT_3:def 4;

A9: dom (.: (pr1 ( the carrier of X, the carrier of Y))) = bool (dom (pr1 ( the carrier of X, the carrier of Y))) by FUNCT_3:def 1

.= bool [: the carrier of X, the carrier of Y:] by FUNCT_3:def 4 ;

e = (pr1 ( the carrier of X, the carrier of Y)) . (x,y) by FUNCT_3:def 4;

then A10: e in (pr1 ( the carrier of X, the carrier of Y)) .: A by A6, A8, FUNCT_1:def 6;

(.: (pr1 ( the carrier of X, the carrier of Y))) . A = (pr1 ( the carrier of X, the carrier of Y)) .: A by A2, A7, EQREL_1:47;

then (pr1 ( the carrier of X, the carrier of Y)) .: A in (Pr1 (X,Y)) .: H by A2, A7, A9, FUNCT_1:def 6;

hence e in union ((Pr1 (X,Y)) .: H) by A10, TARSKI:def 4; :: thesis: verum

end;then consider y being Point of Y such that

A4: y in Y1 by SUBSET_1:4;

let e be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not e in X1 or e in union ((Pr1 (X,Y)) .: H) )

assume A5: e in X1 ; :: thesis: e in union ((Pr1 (X,Y)) .: H)

then reconsider x = e as Point of X ;

[x,y] in [:X1,Y1:] by A4, A5, ZFMISC_1:87;

then consider A being set such that

A6: [x,y] in A and

A7: A in H by A3, TARSKI:def 4;

[x,y] in [: the carrier of X, the carrier of Y:] by ZFMISC_1:87;

then A8: [x,y] in dom (pr1 ( the carrier of X, the carrier of Y)) by FUNCT_3:def 4;

A9: dom (.: (pr1 ( the carrier of X, the carrier of Y))) = bool (dom (pr1 ( the carrier of X, the carrier of Y))) by FUNCT_3:def 1

.= bool [: the carrier of X, the carrier of Y:] by FUNCT_3:def 4 ;

e = (pr1 ( the carrier of X, the carrier of Y)) . (x,y) by FUNCT_3:def 4;

then A10: e in (pr1 ( the carrier of X, the carrier of Y)) .: A by A6, A8, FUNCT_1:def 6;

(.: (pr1 ( the carrier of X, the carrier of Y))) . A = (pr1 ( the carrier of X, the carrier of Y)) .: A by A2, A7, EQREL_1:47;

then (pr1 ( the carrier of X, the carrier of Y)) .: A in (Pr1 (X,Y)) .: H by A2, A7, A9, FUNCT_1:def 6;

hence e in union ((Pr1 (X,Y)) .: H) by A10, TARSKI:def 4; :: thesis: verum

then consider x being Point of X such that

A11: x in X1 by SUBSET_1:4;

let e be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not e in Y1 or e in union ((Pr2 (X,Y)) .: H) )

assume A12: e in Y1 ; :: thesis: e in union ((Pr2 (X,Y)) .: H)

then reconsider y = e as Point of Y ;

[x,y] in [:X1,Y1:] by A11, A12, ZFMISC_1:87;

then consider A being set such that

A13: [x,y] in A and

A14: A in H by A3, TARSKI:def 4;

[x,y] in [: the carrier of X, the carrier of Y:] by ZFMISC_1:87;

then A15: [x,y] in dom (pr2 ( the carrier of X, the carrier of Y)) by FUNCT_3:def 5;

e = (pr2 ( the carrier of X, the carrier of Y)) . (x,y) by FUNCT_3:def 5;

then A16: e in (pr2 ( the carrier of X, the carrier of Y)) .: A by A13, A15, FUNCT_1:def 6;

(.: (pr2 ( the carrier of X, the carrier of Y))) . A = (pr2 ( the carrier of X, the carrier of Y)) .: A by A2, A14, EQREL_1:48;

then (pr2 ( the carrier of X, the carrier of Y)) .: A in (Pr2 (X,Y)) .: H by A2, A14, A1, FUNCT_1:def 6;

hence e in union ((Pr2 (X,Y)) .: H) by A16, TARSKI:def 4; :: thesis: verum