let B, C be Ordinal; :: according to SURREAL1:def 7 :: thesis: ( B in C & C in dom (f /^ A) implies (f /^ A) .. C infinitely< (f /^ A) .. B )
assume A1: ( B in C & C in dom (f /^ A) ) ; :: thesis: (f /^ A) .. C infinitely< (f /^ A) .. B
B in dom (f /^ A) by A1, ORDINAL1:10;
then A2: ( f .. (A +^ B) = (f /^ A) .. B & f .. (A +^ C) = (f /^ A) .. C ) by A1, Th36;
A +^ C in dom f by A1, Th8;
hence (f /^ A) .. C infinitely< (f /^ A) .. B by A2, Def7, A1, ORDINAL2:32; :: thesis: verum