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