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 A1: x in Tarski-Class X,A ; :: thesis: x in Tarski-Class X,(succ A)
A2: 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 ) } by A1;
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 A2, XBOOLE_0:def 3;
A4: 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;
thus x in Tarski-Class X,(succ A) by A3, A4, XBOOLE_0:def 3; :: thesis: verum