let a, b be Ordinal; :: according to SURREALC:def 11 :: thesis: ( a in b & b in dom (s | A) implies for sa, sb being Surreal st sa = (s | A) . a & sb = (s | A) . b holds
sb < sa )
assume A1: ( a in b & b in dom (s | A) ) ; :: thesis: for sa, sb being Surreal st sa = (s | A) . a & sb = (s | A) . b holds
sb < sa
let sa, sb be Surreal; :: thesis: ( sa = (s | A) . a & sb = (s | A) . b implies sb < sa )
assume A2: ( sa = (s | A) . a & sb = (s | A) . b ) ; :: thesis: sb < sa
A3: ( sa = s . a & sb = s . b ) by A1, ORDINAL1:10, A2, FUNCT_1:47;
( a in b & b in dom s ) by A1, RELAT_1:57;
hence sb < sa by A3, Def11; :: thesis: verum