let X be set ; :: thesis: ( Tarski-Class (X,{}) in Tarski-Class (X,1) & Tarski-Class (X,{}) <> Tarski-Class (X,1) )
deffunc H₆( Ordinal) -> Element of bool (Tarski-Class X) = Tarski-Class (X,$1);
deffunc H₇( Ordinal, set ) -> set = ( { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in $2 & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in $2 } ) \/ ((bool $2) /\ (Tarski-Class X));
deffunc H₈( Ordinal, T-Sequence) -> set = (union (rng $2)) /\ (Tarski-Class X);
B1: for A being Ordinal
for x being set holds
( x = H₆(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H₇(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = H₈(C,L | C) ) ) ) by CLASSES1:def 5;
A1: H₆( {} ) = {X} from ORDINAL2:sch 8(B1);
then X in Tarski-Class (X,{}) by TARSKI:def 1;
then A2: bool X in Tarski-Class X by CLASSES1:4;
{X} c= bool X

proof

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

end;

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