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;
A2: X in Tarski-Class X,{} by A1, TARSKI:def 1;
A3: bool X in Tarski-Class X by A2, Th7;
A4: {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 A5: a in {X} ; :: thesis: a in bool X
A6: a = X by A5, TARSKI:def 1;
thus a in bool X by A6, ZFMISC_1:def 1; :: thesis: verum

end;

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