let X, Y be set ; :: thesis: for A being Subset of [:X,Y:]

for H being Subset-Family of [:X,Y:] st ( for E being set st E in H holds

( E c= A & ex X1 being Subset of X ex Y1 being Subset of Y st E = [:X1,Y1:] ) ) holds

[:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A

let A be Subset of [:X,Y:]; :: thesis: for H being Subset-Family of [:X,Y:] st ( for E being set st E in H holds

( E c= A & ex X1 being Subset of X ex Y1 being Subset of Y st E = [:X1,Y1:] ) ) holds

[:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A

let H be Subset-Family of [:X,Y:]; :: thesis: ( ( for E being set st E in H holds

( E c= A & ex X1 being Subset of X ex Y1 being Subset of Y st E = [:X1,Y1:] ) ) implies [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A )

assume A1: for E being set st E in H holds

( E c= A & ex X1 being Subset of X ex Y1 being Subset of Y st E = [:X1,Y1:] ) ; :: thesis: [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A

let u, v be object ; :: according to RELAT_1:def 3 :: thesis: ( not [u,v] in [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] or [u,v] in A )

assume A2: [u,v] in [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] ; :: thesis: [u,v] in A

then A3: v in meet ((.: (pr2 (X,Y))) .: H) by ZFMISC_1:87;

u in union ((.: (pr1 (X,Y))) .: H) by A2, ZFMISC_1:87;

then consider x being set such that

A4: u in x and

A5: x in (.: (pr1 (X,Y))) .: H by TARSKI:def 4;

consider y being object such that

y in dom (.: (pr1 (X,Y))) and

A6: y in H and

A7: x = (.: (pr1 (X,Y))) . y by A5, FUNCT_1:def 6;

reconsider y = y as set by TARSKI:1;

consider X1 being Subset of X, Y1 being Subset of Y such that

A8: y = [:X1,Y1:] by A1, A6;

A9: y <> {} by A4, A7, FUNCT_3:8;

y in bool [:X,Y:] by A6;

then y in bool (dom (pr2 (X,Y))) by FUNCT_3:def 5;

then y in dom (.: (pr2 (X,Y))) by FUNCT_3:def 1;

then (.: (pr2 (X,Y))) . y in (.: (pr2 (X,Y))) .: H by A6, FUNCT_1:def 6;

then Y1 in (.: (pr2 (X,Y))) .: H by A8, A9, Th50;

then A10: v in Y1 by A3, SETFAM_1:def 1;

u in X1 by A4, A7, A8, A9, Th50;

then A11: [u,v] in y by A8, A10, ZFMISC_1:87;

y c= A by A1, A6;

hence [u,v] in A by A11; :: thesis: verum

for H being Subset-Family of [:X,Y:] st ( for E being set st E in H holds

( E c= A & ex X1 being Subset of X ex Y1 being Subset of Y st E = [:X1,Y1:] ) ) holds

[:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A

let A be Subset of [:X,Y:]; :: thesis: for H being Subset-Family of [:X,Y:] st ( for E being set st E in H holds

( E c= A & ex X1 being Subset of X ex Y1 being Subset of Y st E = [:X1,Y1:] ) ) holds

[:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A

let H be Subset-Family of [:X,Y:]; :: thesis: ( ( for E being set st E in H holds

( E c= A & ex X1 being Subset of X ex Y1 being Subset of Y st E = [:X1,Y1:] ) ) implies [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A )

assume A1: for E being set st E in H holds

( E c= A & ex X1 being Subset of X ex Y1 being Subset of Y st E = [:X1,Y1:] ) ; :: thesis: [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A

let u, v be object ; :: according to RELAT_1:def 3 :: thesis: ( not [u,v] in [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] or [u,v] in A )

assume A2: [u,v] in [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] ; :: thesis: [u,v] in A

then A3: v in meet ((.: (pr2 (X,Y))) .: H) by ZFMISC_1:87;

u in union ((.: (pr1 (X,Y))) .: H) by A2, ZFMISC_1:87;

then consider x being set such that

A4: u in x and

A5: x in (.: (pr1 (X,Y))) .: H by TARSKI:def 4;

consider y being object such that

y in dom (.: (pr1 (X,Y))) and

A6: y in H and

A7: x = (.: (pr1 (X,Y))) . y by A5, FUNCT_1:def 6;

reconsider y = y as set by TARSKI:1;

consider X1 being Subset of X, Y1 being Subset of Y such that

A8: y = [:X1,Y1:] by A1, A6;

A9: y <> {} by A4, A7, FUNCT_3:8;

y in bool [:X,Y:] by A6;

then y in bool (dom (pr2 (X,Y))) by FUNCT_3:def 5;

then y in dom (.: (pr2 (X,Y))) by FUNCT_3:def 1;

then (.: (pr2 (X,Y))) . y in (.: (pr2 (X,Y))) .: H by A6, FUNCT_1:def 6;

then Y1 in (.: (pr2 (X,Y))) .: H by A8, A9, Th50;

then A10: v in Y1 by A3, SETFAM_1:def 1;

u in X1 by A4, A7, A8, A9, Th50;

then A11: [u,v] in y by A8, A10, ZFMISC_1:87;

y c= A by A1, A6;

hence [u,v] in A by A11; :: thesis: verum