set S = <%s%>;
let a, b be Ordinal; :: according to SURREALC:def 11 :: thesis: ( a in b & b in dom <%s%> implies for sa, sb being Surreal st sa = <%s%> . a & sb = <%s%> . b holds
sb < sa )
assume A1: ( a in b & b in dom <%s%> ) ; :: thesis: for sa, sb being Surreal st sa = <%s%> . a & sb = <%s%> . b holds
sb < sa
dom <%s%> = {0} by CARD_1:49, AFINSQ_1:33;
hence for sa, sb being Surreal st sa = <%s%> . a & sb = <%s%> . b holds
sb < sa by A1, TARSKI:def 1; :: thesis: verum