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

A5: now

assume A6: A <> B ; :: thesis: x in Tarski-Class X,B
A7: A c< B by A3, A6, XBOOLE_0:def 8;
A8: A in B by A7, 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
A12: ( A c= C & C in B ) by A8, A11, ORDINAL1:34;
A13: Tarski-Class X,A c= Tarski-Class X,C by A2, A12;
A14: Tarski-Class X,C c= Tarski-Class X,B by A11, Th18;
A15: Tarski-Class X,A c= Tarski-Class X,B by A13, A14, XBOOLE_1:1;
thus x in Tarski-Class X,B by A4, A15; :: thesis: verum

end;

A16: now

assume A17: for C being Ordinal holds B <> succ C ; :: thesis: x in Tarski-Class X,B
A18: B is limit_ordinal by A17, ORDINAL1:42;
A19: 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, A18, Th12;
thus x in Tarski-Class X,B by A4, A8, A19; :: thesis: verum

end;

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

end;

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

end;

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