let a, b be real number ; ( 0 <= a & 0 <= b & a <> b implies ((sqrt a) ^2 ) - ((sqrt b) ^2 ) <> 0 )
assume that
A1:
0 <= a
and
A2:
0 <= b
and
A3:
a <> b
; ((sqrt a) ^2 ) - ((sqrt b) ^2 ) <> 0
A4:
0 <= sqrt a
by A1, Def4;
A5:
0 <= sqrt b
by A2, Def4;
sqrt a <> sqrt b
by A1, A2, A3, Th96;
hence
((sqrt a) ^2 ) - ((sqrt b) ^2 ) <> 0
by A4, A5, Lm2; verum