let X be set ; :: thesis: ( Tarski-Class (X,{}) in Tarski-Class (X,1) & Tarski-Class (X,{}) <> Tarski-Class (X,1) )
deffunc H6( Ordinal) -> Element of bool (Tarski-Class X) = Tarski-Class (X,$1);
deffunc H7( 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 H8( Ordinal, Sequence) -> set = (union (rng $2)) /\ (Tarski-Class X);
A1: for A being Ordinal
for x being object holds
( x = H6(A) iff ex L being Sequence st
( x = last L & dom L = succ A & L . 0 = {X} & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = H7(C,L . C) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = H8(C,L | C) ) ) ) by CLASSES1:def 5;
A2: H6( 0 ) = {X} from ORDINAL2:sch 8(A1);
 then X in Tarski-Class (X,{}) by TARSKI:def 1;
then A3: bool X in Tarski-Class X by CLASSES1:4;
{X} c= bool X
proof
let x be object ; :: 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 A3, CLASSES1:3;
hence A4: Tarski-Class (X,{}) in Tarski-Class (X,1) by A2, CLASSES1:10; :: thesis: Tarski-Class (X,{}) <> Tarski-Class (X,1)
assume Tarski-Class (X,{}) = Tarski-Class (X,1) ; :: thesis: contradiction
hence contradiction by A4; :: thesis: verum