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 object ; :: 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 :: thesis: ( A <> B implies x in Tarski-Class (X,B) )

assume A5: A <> B ; :: thesis: x in Tarski-Class (X,B)
then A6: A in B by ORDINAL1:11, A3, XBOOLE_0:def 8;
A7: B <> {} by A3, A5;

A8: now :: thesis: ( ex C being Ordinal st B = succ C implies x in Tarski-Class (X,B) )

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:22;
then A10: Tarski-Class (X,A) c= Tarski-Class (X,C) by A2;
Tarski-Class (X,C) c= Tarski-Class (X,B) by A9, Th15;
then Tarski-Class (X,A) c= Tarski-Class (X,B) by A10;
hence x in Tarski-Class (X,B) by A4; :: thesis: verum

end;

now :: thesis: ( ( for C being Ordinal holds B <> succ C ) implies x in Tarski-Class (X,B) )

assume for C being Ordinal holds B <> succ C ; :: thesis: x in Tarski-Class (X,B)
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, Th9, ORDINAL1:29;
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