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