let X, Y be non empty TopSpace; :: 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

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

hence [:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A by A1, EQREL_1:51; :: 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

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

hence [:(union ((Pr1 (X,Y)) .: H)),(meet ((Pr2 (X,Y)) .: H)):] c= A by A1, EQREL_1:51; :: thesis: verum