theorem :: SURREALO:25

for X being set
for x, y, z, t being Surreal st x <= y & z = [{x,y},X] & t = [{y},X] holds
z == t