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