let A, B be Ordinal; :: thesis: ( A in B implies ( B -^ A <> {} & {} in B -^ A ) )
assume A in B ; :: thesis: ( B -^ A <> {} & {} in B -^ A )
then A -^ A in B -^ A by Th66;
hence ( B -^ A <> {} & {} in B -^ A ) by Th67; :: thesis: verum