let x, y, z be Surreal; :: thesis: ( |.x.| infinitely< z & |.y.| infinitely< z implies |.(x - y).| infinitely< z )
assume A1: ( |.x.| infinitely< z & |.y.| infinitely< z ) ; :: thesis: |.(x - y).| infinitely< z
then |.(- y).| infinitely< z by Th42;
hence |.(x - y).| infinitely< z by Th41, A1; :: thesis: verum