theorem Th50: :: EQREL_1:50

for X, Y being set
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 )