let B, C be Ordinal; :: thesis: for A being epsilon-transitive set st A in B & B in C holds
A in C
let A be epsilon-transitive set ; :: thesis: ( A in B & B in C implies A in C )
assume A1: ( A in B & B in C ) ; :: thesis: A in C
then B c= C by Def2;
hence A in C by A1; :: thesis: verum