let a2, a3, c2 be Real; :: thesis: ( a2 <> a3 & c2 <> 0 implies (a3 * c2) - (a2 * c2) <> 0 )
assume A1: ( a2 <> a3 & c2 <> 0 ) ; :: thesis: (a3 * c2) - (a2 * c2) <> 0
A2: (a3 * c2) - (a2 * c2) = (a3 - a2) * c2 ;
a3 - a2 <> 0 by A1;
hence (a3 * c2) - (a2 * c2) <> 0 by A1, A2, XCMPLX_1:6; :: thesis: verum