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