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

proof

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

end;

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