theorem Th105: :: SURREALC:105

for x being Surreal holds
( dom (name-r x) = name-ord x & name-ord x = dom (name-y x) )