let X be set ; :: thesis: ( X is epsilon-transitive implies for A being Ordinal st A <> {} holds
Tarski-Class (X,A) is epsilon-transitive )
assume A1: for Y being set st Y in X holds
Y c= X ; :: according to ORDINAL1:def 2 :: thesis: for A being Ordinal st A <> {} holds
Tarski-Class (X,A) is epsilon-transitive
defpred S₁[ Ordinal] means ( $1 <> {} implies Tarski-Class (X,$1) is epsilon-transitive );
A2: for A being Ordinal st ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A3: for B being Ordinal st B in A holds
S₁[B] and
A4: A <> {} ; :: thesis: Tarski-Class (X,A) is epsilon-transitive
let Y be set ; :: according to ORDINAL1:def 2 :: thesis: ( not Y in Tarski-Class (X,A) or Y c= Tarski-Class (X,A) )
assume A5: Y in Tarski-Class (X,A) ; :: thesis: Y c= Tarski-Class (X,A)

A6: now

given B being Ordinal such that A7: A = succ B ; :: thesis: Y c= Tarski-Class (X,A)
B in A by A7, ORDINAL1:6;
then A8: B c= A by ORDINAL1:def 2;
A9: S₁[B] by A3, A7, ORDINAL1:6;
A10: Tarski-Class (X,B) c= Tarski-Class (X,A) by A8, Th19;

now

assume not Y c= Tarski-Class (X,B) ; :: thesis: Y c= Tarski-Class (X,A)
then consider Z being set such that
A11: Z in Tarski-Class (X,B) and
A12: ( Y c= Z or Y = bool Z ) by A5, A7, Th13;

A13: now

assume A14: Y = bool Z ; :: thesis: Y c= Tarski-Class (X,A)
thus Y c= Tarski-Class (X,A) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in Tarski-Class (X,A) )
assume x in Y ; :: thesis: x in Tarski-Class (X,A)
hence x in Tarski-Class (X,A) by A7, A11, A14, Th13; :: thesis: verum

end;

end;

now

assume A15: Y c= Z ; :: thesis: Y c= Tarski-Class (X,A)
thus Y c= Tarski-Class (X,A) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in Tarski-Class (X,A) )
assume A16: x in Y ; :: thesis: x in Tarski-Class (X,A)
then A17: x in Z by A15;

A18: now

assume B = {} ; :: thesis: x in Tarski-Class (X,A)
then Tarski-Class (X,B) = {X} by Lm1;
then A19: Z = X by A11, TARSKI:def 1;
then x c= X by A1, A15, A16;
hence x in Tarski-Class (X,A) by A7, A11, A19, Th13; :: thesis: verum

end;

now

assume B <> {} ; :: thesis: x in Tarski-Class (X,A)
then Z c= Tarski-Class (X,B) by A9, A11, ORDINAL1:def 2;
then x in Tarski-Class (X,B) by A17;
hence x in Tarski-Class (X,A) by A10; :: thesis: verum

end;

hence x in Tarski-Class (X,A) by A18; :: thesis: verum

end;

end;

hence Y c= Tarski-Class (X,A) by A12, A13; :: thesis: verum

end;

hence Y c= Tarski-Class (X,A) by A10, XBOOLE_1:1; :: thesis: verum

end;

now

assume A20: for B being Ordinal holds A <> succ B ; :: thesis: Y c= Tarski-Class (X,A)
then A is limit_ordinal by ORDINAL1:29;
then consider B being Ordinal such that
A21: B in A and
A22: Y in Tarski-Class (X,B) by A4, A5, Th16;
A23: succ B c= A by A21, ORDINAL1:21;
A24: succ B <> A by A20;
A25: Tarski-Class (X,B) c= Tarski-Class (X,(succ B)) by Th18;
A26: succ B c< A by A23, A24, XBOOLE_0:def 8;
A27: Tarski-Class (X,(succ B)) c= Tarski-Class (X,A) by A23, Th19;
Tarski-Class (X,(succ B)) is epsilon-transitive by A3, A26, ORDINAL1:11;
then Y c= Tarski-Class (X,(succ B)) by A22, A25, ORDINAL1:def 2;
hence Y c= Tarski-Class (X,A) by A27, XBOOLE_1:1; :: thesis: verum

end;

hence Y c= Tarski-Class (X,A) by A6; :: thesis: verum

end;

thus for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A2); :: thesis: verum