theorem :: BORSUK_1:24

for X, Y being non empty TopSpace
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (Pr1 (X,Y)) . [:X1,Y1:] = X1 & (Pr2 (X,Y)) . [:X1,Y1:] = Y1 ) by EQREL_1:50;