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