theorem :: XBOOLE_1:14

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