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 )
A1: the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:] by Def5;
assume 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
hence [:(union ((Pr1 X,Y) .: H)),(meet ((Pr2 X,Y) .: H)):] c= A by A1, Th14; :: thesis: verum