let A, B be Ordinal; :: thesis: ( A c= B or B in A )
( A in B or A = B or B in A ) by Th10;
hence ( A c= B or B in A ) by Def2; :: thesis: verum