let x, y be Surreal; :: thesis: ( not x == 0_No & not y == 0_No implies ( omega-y x = omega-y y iff |.x.|,|.y.| are_commensurate ) )
assume A1: ( not x == 0_No & not y == 0_No ) ; :: thesis: ( omega-y x = omega-y y iff |.x.|,|.y.| are_commensurate )
then A2: ( |.x.|, No_omega^ (omega-y x) are_commensurate & |.y.|, No_omega^ (omega-y y) are_commensurate ) by Def7;
thus ( omega-y x = omega-y y implies |.x.|,|.y.| are_commensurate ) by A2, Th4; :: thesis: ( |.x.|,|.y.| are_commensurate implies omega-y x = omega-y y )
assume |.x.|,|.y.| are_commensurate ; :: thesis: omega-y x = omega-y y
then |.y.|, No_omega^ (omega-y x) are_commensurate by A2, Th4;
hence omega-y x = omega-y y by A1, Def7; :: thesis: verum