theorem Th233: :: XREAL_1:233

for a, b being Real st b <= a holds
a -' b = a - b by Th48, XREAL_0:def 2;