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 * ()) + (b2 * ()) <> 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 * ()) + (b2 * ()) <> 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 * ()) + (b2 * ()) <> 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 * ()) + (b2 * ()) <> 0 )

consider q being Element of RAT such that
A2: denominator q > [\r1/] + 1 and
A3: q in HWZSet r by Th42;
per cases ) + (b2 * ()) <> 0 or (a2 * ()) + (b2 * ()) = 0 ) ;
suppose (a2 * ()) + (b2 * ()) <> 0 ; :: thesis: ex q being Element of RAT st
( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * ()) + (b2 * ()) <> 0 )

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

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