theorem Th12: :: XBOOLE_1:12

for X, Y being set st X c= Y holds
X \/ Y = Y