let x1, x2, x3, x4, X be set ; :: thesis: ( {x1,x2,x3,x4} c= X iff ( x1 in X & x2 in X & x3 in X & x4 in X ) )
A1: x1 in {x1,x2,x3,x4} by ENUMSET1:def 2;
A2: x2 in {x1,x2,x3,x4} by ENUMSET1:def 2;
A3: x3 in {x1,x2,x3,x4} by ENUMSET1:def 2;
x4 in {x1,x2,x3,x4} by ENUMSET1:def 2;
hence ( {x1,x2,x3,x4} c= X implies ( x1 in X & x2 in X & x3 in X & x4 in X ) ) by A1, A2, A3; :: thesis: ( x1 in X & x2 in X & x3 in X & x4 in X implies {x1,x2,x3,x4} c= X )
assume that
A4: x1 in X and
A5: x2 in X and
A6: x3 in X and
A7: x4 in X ; :: thesis: {x1,x2,x3,x4} c= X
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {x1,x2,x3,x4} or z in X )
assume z in {x1,x2,x3,x4} ; :: thesis: z in X
hence z in X by A4, A5, A6, A7, ENUMSET1:def 2; :: thesis: verum