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 be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [u,b₁] in [:(meet ((.: (pr1 X,Y)) .: H)),(union ((.: (pr2 X,Y)) .: H)):] or [u,b₁] in A )
let v be set ; :: thesis: ( not [u,v] in [:(meet ((.: (pr1 X,Y)) .: H)),(union ((.: (pr2 X,Y)) .: H)):] or [u,v] in A )
assume [u,v] in [:(meet ((.: (pr1 X,Y)) .: H)),(union ((.: (pr2 X,Y)) .: H)):] ; :: thesis: [u,v] in A
then A2: ( u in meet ((.: (pr1 X,Y)) .: H) & v in union ((.: (pr2 X,Y)) .: H) ) by ZFMISC_1:106;
then consider x being set such that
A3: ( v in x & x in (.: (pr2 X,Y)) .: H ) by TARSKI:def 4;
consider y being set such that
A4: ( y in dom (.: (pr2 X,Y)) & y in H & x = (.: (pr2 X,Y)) . y ) by A3, FUNCT_1:def 12;
consider X1 being Subset of X, Y1 being Subset of Y such that
A5: y = [:X1,Y1:] by A1, A4;
A6: y <> {} by A3, A4, FUNCT_3:9;
y in bool [:X,Y:] by A4;
then y in bool (dom (pr1 X,Y)) by FUNCT_3:def 5;
then y in dom (.: (pr1 X,Y)) by FUNCT_3:def 1;
then (.: (pr1 X,Y)) . y in (.: (pr1 X,Y)) .: H by A4, FUNCT_1:def 12;
then X1 in (.: (pr1 X,Y)) .: H by A5, A6, Th13;
then ( u in X1 & v in Y1 ) by A2, A3, A4, A5, A6, Th13, SETFAM_1:def 1;
then A7: [u,v] in y by A5, ZFMISC_1:106;
y c= A by A1, A4;
hence [u,v] in A by A7; :: thesis: verum