theorem Th16: :: BORSUK_1:16
for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:]
for C being set st C in (Pr1 (X,Y)) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 ( the carrier of X, the carrier of Y)) .: D )