let X be set ; :: thesis: ( Tarski-Class (X,{}) in Tarski-Class (X,1) & Tarski-Class (X,{}) <> Tarski-Class (X,1) )
A1: Tarski-Class (X,{}) = {X} by Lm1;
then X in Tarski-Class (X,{}) by TARSKI:def 1;
then A3: bool X in Tarski-Class X by Th7;
{X} c= bool X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {X} or a in bool X )
assume a in {X} ; :: thesis: a in bool X
then a = X by TARSKI:def 1;
hence a in bool X by ZFMISC_1:def 1; :: thesis: verum

end;

then ( 1 = succ 0 & {X} in Tarski-Class X ) by A3, Th6;
hence A8: Tarski-Class (X,{}) in Tarski-Class (X,1) by A1, Th13; :: thesis: Tarski-Class (X,{}) <> Tarski-Class (X,1)
assume Tarski-Class (X,{}) = Tarski-Class (X,1) ; :: thesis: contradiction
hence contradiction by A8; :: thesis: verum