let A be epsilon-transitive set ; :: thesis: for B, C being Ordinal st A c= B & B in C holds
A in C
let B, C be Ordinal; :: thesis: ( A c= B & B in C implies A in C )
assume A1: ( A c= B & B in C ) ; :: thesis: A in C
then B c= C by Def2;
then ( A c= C & A <> C ) by A1, Th7, XBOOLE_1:1;
then A c< C by XBOOLE_0:def 8;
hence A in C by Th21; :: thesis: verum