let x, Z, y be set ; :: thesis: ( x in Z & y in Z implies {x,y} \/ Z = Z )
assume ( x in Z & y in Z ) ; :: thesis: {x,y} \/ Z = Z
then {x,y} c= Z by Th38;
hence {x,y} \/ Z = Z by XBOOLE_1:12; :: thesis: verum