let r be irrational Real; :: thesis: for a1, a2, b1, b2 being Element of REAL
for r1 being non negative Real st |.((a1 * b2) - (a2 * b1)).| <> 0 holds
ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )
let a1, a2, b1, b2 be Element of REAL ; :: thesis: for r1 being non negative Real st |.((a1 * b2) - (a2 * b1)).| <> 0 holds
ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )
let r1 be non negative Real; :: thesis: ( |.((a1 * b2) - (a2 * b1)).| <> 0 implies ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 ) )
assume A1: |.((a1 * b2) - (a2 * b1)).| <> 0 ; :: thesis: ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )
consider q being Element of RAT such that
A2: denominator q > [\r1/] + 1 and
A3: q in HWZSet r by Th42;

per cases ( (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 or (a2 * (denominator q)) + (b2 * (numerator q)) = 0 ) ;

suppose (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 ; :: thesis: ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

hence ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 ) by A2, A3; :: thesis: verum

end;

suppose A5: (a2 * (denominator q)) + (b2 * (numerator q)) = 0 ; :: thesis: ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

consider q1 being Element of RAT such that
A6: denominator q1 > [\(denominator q)/] + 1 and
A7: q1 in HWZSet r by Th42;
denominator q1 > denominator q by A6, INT_1:29, XXREAL_0:2;
then A8: denominator q1 > [\r1/] + 1 by A2, XXREAL_0:2;
q1 <> q by A6, INT_1:29;
then (a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0 by A1, A5, Th43;
hence ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 ) by A7, A8; :: thesis: verum

end;

end;