{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} c= MC-wff

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} or x in MC-wff )
assume x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} ; :: thesis: x in MC-wff
then ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) by ENUMSET1:def 8;
hence x in MC-wff ; :: thesis: verum

end;

hence {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} is Subset of MC-wff ; :: thesis: verum