let x, y be Surreal; :: thesis: for X, Y being set st x == y holds
divset (X,x,Y) <=_ divset (X,y,Y)
let X, Y be set ; :: thesis: ( x == y implies divset (X,x,Y) <=_ divset (X,y,Y) )
assume A1: x == y ; :: thesis: divset (X,x,Y) <=_ divset (X,y,Y)
let z be Surreal; :: according to SURREALO:def 3 :: thesis: ( not z in divset (X,x,Y) or ex b₁, b₂ being set st
( b₁ in divset (X,y,Y) & b₂ in divset (X,y,Y) & b₁ <= z & z <= b₂ ) )
assume z in divset (X,x,Y) ; :: thesis: ex b₁, b₂ being set st
( b₁ in divset (X,y,Y) & b₂ in divset (X,y,Y) & b₁ <= z & z <= b₂ )
then consider x1, y1 being Surreal such that
A2: ( 0_No < x1 & x1 in X & y1 in Y ) and
A3: z = (1_No + ((x1 - x) * y1)) * (x1 ") by Def15;
A4: (1_No + ((x1 - y) * y1)) * (x1 ") in divset (X,y,Y) by A2, Def15;
- x == - y by A1, SURREALR:10;
then x1 + (- x) == x1 + (- y) by SURREALR:43;
then (x1 + (- x)) * y1 == (x1 + (- y)) * y1 by SURREALR:51;
then 1_No + ((x1 + (- x)) * y1) == 1_No + ((x1 + (- y)) * y1) by SURREALR:43;
then z == (1_No + ((x1 + (- y)) * y1)) * (x1 ") by A3, SURREALR:51;
hence ex b₁, b₂ being set st
( b₁ in divset (X,y,Y) & b₂ in divset (X,y,Y) & b₁ <= z & z <= b₂ ) by A4; :: thesis: verum