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:10;
then A8: ( B c= A & S₁[B] ) by A3, ORDINAL1:def 2;
then A9: Tarski-Class X,B c= Tarski-Class X,A by Th19;

now

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

A11: now

assume A12: 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, A10, A12, Th13; :: thesis: verum

end;

end;

now

assume A13: 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 A14: x in Y ; :: thesis: x in Tarski-Class X,A
then A15: x in Z by A13;

A16: now

assume B = {} ; :: thesis: x in Tarski-Class X,A
then Tarski-Class X,B = {X} by Lm1;
then A17: Z = X by A10, TARSKI:def 1;
then x c= X by A1, A13, A14;
hence x in Tarski-Class X,A by A7, A10, A17, Th13; :: thesis: verum

end;

now

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

end;

hence x in Tarski-Class X,A by A16; :: thesis: verum

end;

end;

hence Y c= Tarski-Class X,A by A10, A11; :: thesis: verum

end;

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

end;

now

assume A18: for B being Ordinal holds A <> succ B ; :: thesis: Y c= Tarski-Class X,A
then A is limit_ordinal by ORDINAL1:42;
then consider B being Ordinal such that
A19: ( B in A & Y in Tarski-Class X,B ) by A4, A5, Th16;
A20: ( succ B c= A & succ B <> A & succ B <> {} & Tarski-Class X,B c= Tarski-Class X,(succ B) ) by A18, A19, Th18, ORDINAL1:33;
then succ B c< A by XBOOLE_0:def 8;
then A21: ( succ B in A & succ B <> {} & Y in Tarski-Class X,(succ B) & Tarski-Class X,(succ B) c= Tarski-Class X,A ) by A19, A20, Th19, ORDINAL1:21;
then Tarski-Class X,(succ B) is epsilon-transitive by A3;
then Y c= Tarski-Class X,(succ B) by A19, A20, ORDINAL1:def 2;
hence Y c= Tarski-Class X,A by A21, 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