let A, B be Ordinal; :: thesis: ( A in B implies ex C being Ordinal st
( B = A +^ C & C <> {} ) )
assume A1: A in B ; :: thesis: ex C being Ordinal st
( B = A +^ C & C <> {} )
then A c= B by ORDINAL1:def 2;
then consider C being Ordinal such that
A2: B = A +^ C by Th27;
take C ; :: thesis: ( B = A +^ C & C <> {} )
thus B = A +^ C by A2; :: thesis: C <> {}
assume C = {} ; :: thesis: contradiction
then B = A by A2, ORDINAL2:27;
hence contradiction by A1; :: thesis: verum