let o be object ; :: thesis: for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds
sqrt (o,X1,Y1) c= sqrt (o,X2,Y2)
let X1, X2, Y1, Y2 be set ; :: thesis: ( X1 c= X2 & Y1 c= Y2 implies sqrt (o,X1,Y1) c= sqrt (o,X2,Y2) )
assume A1: ( X1 c= X2 & Y1 c= Y2 ) ; :: thesis: sqrt (o,X1,Y1) c= sqrt (o,X2,Y2)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in sqrt (o,X1,Y1) or a in sqrt (o,X2,Y2) )
assume a in sqrt (o,X1,Y1) ; :: thesis: a in sqrt (o,X2,Y2)
then ex x1, y1 being Surreal st
( x1 in X1 & y1 in Y1 & not x1 + y1 == 0_No & a = (o +' (x1 * y1)) * ((x1 + y1) ") ) by Def2;
hence a in sqrt (o,X2,Y2) by A1, Def2; :: thesis: verum