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
[:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (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
[:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (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 [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (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: [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A
let u, v be object ; :: according to RELAT_1:def 3 :: thesis: ( not [u,v] in [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] or [u,v] in A )
assume A2: [u,v] in [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] ; :: thesis: [u,v] in A
then A3: u in meet ((.: (pr1 (X,Y))) .: H) by ZFMISC_1:87;
v in union ((.: (pr2 (X,Y))) .: H) by A2, ZFMISC_1:87;
then consider x being set such that
A4: v in x and
A5: x in (.: (pr2 (X,Y))) .: H by TARSKI:def 4;
consider y being object such that
y in dom (.: (pr2 (X,Y))) and
A6: y in H and
A7: x = (.: (pr2 (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 (pr1 (X,Y))) by FUNCT_3:def 4;
then y in dom (.: (pr1 (X,Y))) by FUNCT_3:def 1;
then (.: (pr1 (X,Y))) . y in (.: (pr1 (X,Y))) .: H by A6, FUNCT_1:def 6;
then X1 in (.: (pr1 (X,Y))) .: H by A8, A9, Th50;
then A10: u in X1 by A3, SETFAM_1:def 1;
v in Y1 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