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