theorem :: XBOOLE_1:20

for X, Y, Z being set st X c= Y & X c= Z & ( for V being set st V c= Y & V c= Z holds
V c= X ) holds
X = Y /\ Z