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 & A -^ A = {} ) by Th66, Th67;
hence ( B -^ A <> {} & {} in B -^ A ) ; :: thesis: verum