let x be Surreal; :: thesis: name-r x, name-y x, name-ord x name_like x
name-ord x = dom (name-r x) by Th105;
then A2: name-r x, name-y x, name-ord x name_like Sum ((name-r x),(name-y x)) by Def23, Th101;
Sum ((name-r x),(name-y x)) == x by Def23;
hence name-r x, name-y x, name-ord x name_like x by A2, Th103; :: thesis: verum