let A be epsilon-transitive set ; for B, C being Ordinal st A c= B & B in C holds
A in C
let B, C be Ordinal; ( A c= B & B in C implies A in C )
assume that
A1:
A c= B
and
A2:
B in C
; A in C
B c= C
by A2, Def2;
then A3:
A c= C
by A1;
A <> C
by A1, A2, Th1;
then
A c< C
by A3;
hence
A in C
by Th7; verum