theorem :: SQUARE_1:35

for a, b being Real st 0 <= a & 0 <= b holds
((sqrt a) - (sqrt b)) * ((sqrt a) + (sqrt b)) = a - b