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 Th53;
hence ( B -^ A <> {} & {} in B -^ A ) by Th54; :: thesis: verum