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 set ; :: 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 A3: 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 A3, XBOOLE_0:def 3; :: thesis: verum