let x, y be Surreal; :: thesis: for X being set holds comp (X,x,y,{}) = {}
let X be set ; :: thesis: comp (X,x,y,{}) = {}
assume comp (X,x,y,{}) <> {} ; :: thesis: contradiction
then consider o being object such that
A1: o in comp (X,x,y,{}) by XBOOLE_0:def 1;
consider x1, y1 being Surreal such that
A2: ( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in {} ) by A1, Def14;
thus contradiction by A2; :: thesis: verum