let x be Surreal; :: thesis: ( dom (name-r x) = name-ord x & name-ord x = dom (name-y x) )
( dom (name-r x) = dom (name-y x) & Sum ((name-r x),(name-y x)) == x ) by Def23;
hence ( dom (name-r x) = name-ord x & name-ord x = dom (name-y x) ) by Th104; :: thesis: verum