let a, b, c be object ; :: thesis: for A being set holds
( {a,b,c} c= A iff ( a in A & b in A & c in A ) )
let A be set ; :: thesis: ( {a,b,c} c= A iff ( a in A & b in A & c in A ) )
set X = {a,b,c};
( a in {a,b,c} & b in {a,b,c} & c in {a,b,c} ) by ENUMSET1:def 1;
hence ( {a,b,c} c= A implies ( a in A & b in A & c in A ) ) ; :: thesis: ( a in A & b in A & c in A implies {a,b,c} c= A )
assume A1: ( a in A & b in A & c in A ) ; :: thesis: {a,b,c} c= A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a,b,c} or x in A )
thus ( not x in {a,b,c} or x in A ) by A1, ENUMSET1:def 1; :: thesis: verum