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 A5: A <> B ; :: thesis: x in Tarski-Class X,B
then A c< B by A3, XBOOLE_0:def 8;
then A6: A in B by ORDINAL1:21;
A7: B <> {} by A3, A5;

A8: now

given C being Ordinal such that A9: B = succ C ; :: thesis: x in Tarski-Class X,B
( A c= C & C in B ) by A6, A9, ORDINAL1:34;
then ( Tarski-Class X,A c= Tarski-Class X,C & Tarski-Class X,C c= Tarski-Class X,B ) by A2, A9, Th18;
then Tarski-Class X,A c= Tarski-Class X,B by 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 A7, Th12;
hence x in Tarski-Class X,B by A4, A6; :: thesis: verum

end;

hence x in Tarski-Class X,B by A8; :: 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