let X be set ; :: thesis: for A being Ordinal holds Tarski-Class (X,A) c= Tarski-Class (X,(succ A))
let A be Ordinal; :: thesis: Tarski-Class (X,A) c= Tarski-Class (X,(succ A))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Tarski-Class (X,A) or x in Tarski-Class (X,(succ A)) )
assume x in Tarski-Class (X,A) ; :: thesis: x in Tarski-Class (X,(succ A))
then x in { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v ) } ;
then A1: x in { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A) } by XBOOLE_0:def 3;
Tarski-Class (X,(succ A)) = ( { u where u is Element of Tarski-Class X : ex v being Element of Tarski-Class X st
( v in Tarski-Class (X,A) & u c= v ) } \/ { (bool v) where v is Element of Tarski-Class X : v in Tarski-Class (X,A) } ) \/ ((bool (Tarski-Class (X,A))) /\ (Tarski-Class X)) by Lm1;
hence x in Tarski-Class (X,(succ A)) by A1, XBOOLE_0:def 3; :: thesis: verum