let a, b be Real; :: thesis: ( 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 ; :: thesis: ((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; :: thesis: verum

assume that

A1: 0 <= a and

A2: 0 <= b and

A3: a <> b ; :: thesis: ((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; :: thesis: verum