let a, b be Real; :: thesis: ( 0 <= a & 0 <= b implies 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b) )
assume that
A1: 0 <= a and
A2: 0 <= b ; :: thesis: 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)

per cases ( a <> b or a = b ) ;

suppose a <> b ; :: thesis: 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)

hence 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (((sqrt a) ^2) - ((sqrt b) ^2)) by A1, A2, Lm5, Th11
.= ((sqrt a) + (sqrt b)) / (a - ((sqrt b) ^2)) by A1, Def2
.= ((sqrt a) + (sqrt b)) / (a - b) by A2, Def2 ;
:: thesis: verum

end;

suppose A3: a = b ; :: thesis: 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)

then 1 / ((sqrt a) - (sqrt b)) = 0 ;
hence 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b) by A3; :: thesis: verum

end;

end;