let X be set ; :: thesis: for A, B being Ordinal st A c= B holds
Tarski-Class X,A c= Tarski-Class X,B
let A, B be Ordinal; :: thesis: ( A c= B implies Tarski-Class X,A c= Tarski-Class X,B )
defpred S₁[ Ordinal] means ( A c= $1 implies Tarski-Class X,A c= Tarski-Class X,$1 );
A1: for B being Ordinal st ( for C being Ordinal st C in B holds
S₁[C] ) holds
S₁[B]

proof

let B be Ordinal; :: thesis: ( ( for C being Ordinal st C in B holds
S₁[C] ) implies S₁[B] )
assume that
A2: for C being Ordinal st C in B holds
S₁[C] and
A3: A c= B ; :: thesis: Tarski-Class X,A c= Tarski-Class X,B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Tarski-Class X,A or x in Tarski-Class X,B )
assume A4: x in Tarski-Class X,A ; :: thesis: x in Tarski-Class X,B

now

assume A6: A <> B ; :: thesis: x in Tarski-Class X,B
then A c< B by A3, XBOOLE_0:def 8;
then A8: A in B by ORDINAL1:21;
A9: B <> {} by A3, A6;

A10: now

given C being Ordinal such that A11: B = succ C ; :: thesis: x in Tarski-Class X,B
( A c= C & C in B ) by A8, A11, ORDINAL1:34;
then A13: Tarski-Class X,A c= Tarski-Class X,C by A2;
Tarski-Class X,C c= Tarski-Class X,B by A11, Th18;
then Tarski-Class X,A c= Tarski-Class X,B by A13, XBOOLE_1:1;
hence x in Tarski-Class X,B by A4; :: thesis: verum

end;

now

assume for C being Ordinal holds B <> succ C ; :: thesis: x in Tarski-Class X,B
then B is limit_ordinal by ORDINAL1:42;
then Tarski-Class X,B = { v where v is Element of Tarski-Class X : ex C being Ordinal st
( C in B & v in Tarski-Class X,C ) } by A9, Th12;
hence x in Tarski-Class X,B by A4, A8; :: thesis: verum

end;

hence x in Tarski-Class X,B by A10; :: thesis: verum

end;

hence x in Tarski-Class X,B by A4; :: thesis: verum

end;

for B being Ordinal holds S₁[B] from ORDINAL1:sch 2(A1);
hence ( A c= B implies Tarski-Class X,A c= Tarski-Class X,B ) ; :: thesis: verum