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 A9: B c= A by ORDINAL1:def 2;
A10: S₁[B] by A3, A7, ORDINAL1:10;
A11: Tarski-Class X,B c= Tarski-Class X,A by A9, Th19;

now

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

A16: now

assume A17: 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, A14, A17, Th13; :: thesis: verum

end;

end;

now

assume A20: 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 A21: x in Y ; :: thesis: x in Tarski-Class X,A
then A22: x in Z by A20;

A23: now

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

end;

now

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

end;

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

end;

end;

hence Y c= Tarski-Class X,A by A15, A16; :: thesis: verum

end;

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

end;

now

assume A33: 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
A35: B in A and
A36: Y in Tarski-Class X,B by A4, A5, Th16;
A37: succ B c= A by A35, ORDINAL1:33;
A38: succ B <> A by A33;
A39: Tarski-Class X,B c= Tarski-Class X,(succ B) by Th18;
A40: succ B c< A by A37, A38, XBOOLE_0:def 8;
A41: Tarski-Class X,(succ B) c= Tarski-Class X,A by A37, Th19;
Tarski-Class X,(succ B) is epsilon-transitive by A3, A40, ORDINAL1:21;
then Y c= Tarski-Class X,(succ B) by A36, A39, ORDINAL1:def 2;
hence Y c= Tarski-Class X,A by A41, 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