let a, b, c, X be set ; :: thesis: ( a in X & b in X & c in X implies {a,b,c} c= X )
assume ( a in X & b in X & c in X ) ; :: thesis: {a,b,c} c= X
then ( {a,b} c= X & {c} c= X ) by Lm1, Th31;
then {a,b} \/ {c} c= X by XBOOLE_1:8;
hence {a,b,c} c= X by ENUMSET1:3; :: thesis: verum