:: deftheorem defines >>= SURREAL0:def 2 :
for L, R, O being set holds
( L >>= O,R iff for l, r being object st l in L & r in R holds
l >= O,r );