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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {x1,x2,x3,x4,x5,x6,x7} or x in MC-wff )
assume x in {x1,x2,x3,x4,x5,x6,x7} ; :: 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 ) by ENUMSET1:def 5;
hence x in MC-wff ; :: thesis: verum

end;

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