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

A12: now

assume A13: not Y c= Tarski-Class X,B ; :: thesis: Y c= Tarski-Class X,A
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, A13, 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 A18: x in Y ; :: thesis: x in Tarski-Class X,A
thus x in Tarski-Class X,A by A7, A14, A17, A18, Th13; :: thesis: verum

end;

end;

A19: 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
A22: x in Z by A20, A21;

A23: now

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

end;

A28: now

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

end;

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

end;

end;

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

end;

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

end;

A32: now

assume A33: for B being Ordinal holds A <> succ B ; :: thesis: Y c= Tarski-Class X,A
A34: A is limit_ordinal by A33, ORDINAL1:42;
consider B being Ordinal such that
A35: B in A and
A36: Y in Tarski-Class X,B by A4, A5, A34, 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;
A42: Tarski-Class X,(succ B) is epsilon-transitive by A3, A40, ORDINAL1:21;
A43: Y c= Tarski-Class X,(succ B) by A36, A39, A42, ORDINAL1:def 2;
thus Y c= Tarski-Class X,A by A41, A43, XBOOLE_1:1; :: thesis: verum

end;

thus Y c= Tarski-Class X,A by A6, A32; :: thesis: verum

end;

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