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 ZFMISC_1:37, ZFMISC_1:38;
then {a,b} \/ {c} c= X by XBOOLE_1:8;
hence {a,b,c} c= X by ENUMSET1:43; :: thesis: verum