let a, b be real number ; :: thesis: ( 0 <= a & 0 <= b & a <> b implies ((sqrt a) ^2 ) - ((sqrt b) ^2 ) <> 0 )
assume ( 0 <= a & 0 <= b & a <> b ) ; :: thesis: ((sqrt a) ^2 ) - ((sqrt b) ^2 ) <> 0
then ( sqrt a <> sqrt b & 0 <= sqrt a & 0 <= sqrt b ) by Def4, Th96;
hence ((sqrt a) ^2 ) - ((sqrt b) ^2 ) <> 0 by Lm2; :: thesis: verum