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 that
A1: A in B +^ C and
A2: not A in B ; :: thesis: ex D being Ordinal st
( D in C & A = B +^ D )
consider D being Ordinal such that
A3: A = B +^ D by A2, Th27, ORDINAL1:16;
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 A3, ORDINAL1:16;
hence contradiction by A1, A3, ORDINAL1:5, ORDINAL2:33; :: thesis: verum