theorem Th15: :: BORSUK_1:15

for X, Y being non empty TopSpace
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