let a, b be Real; ( 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, Def2;
A5:
0 <= sqrt b
by A2, Def2;
sqrt a <> sqrt b
by A1, A2, A3, Th28;
hence
((sqrt a) ^2) - ((sqrt b) ^2) <> 0
by A4, A5, Lm2; verum