let A, B be Ordinal; :: thesis: ( A in B implies B = A +^ (B -^ A) )
assume A in B ; :: thesis: B = A +^ (B -^ A)
then A c= B by ORDINAL1:def 2;
hence B = A +^ (B -^ A) by Def5; :: thesis: verum