let A, B, C be Ordinal; :: thesis: ( not A in B +^ C or A in B or ex D being Ordinal st
( D in C & A = B +^ D ) )
assume A1: ( A in B +^ C & not A in B ) ; :: thesis: ex D being Ordinal st
( D in C & A = B +^ D )
then B c= A by ORDINAL1:26;
then consider D being Ordinal such that
A2: A = B +^ D by Th30;
take D ; :: thesis: ( D in C & A = B +^ D )
assume ( not D in C or not A = B +^ D ) ; :: thesis: contradiction
then C c= D by A2, ORDINAL1:26;
hence contradiction by A1, A2, ORDINAL1:7, ORDINAL2:50; :: thesis: verum