let F be Field; for a, b, c, d, e, h being Element of F st b <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F holds
(d * c) - (h * e) = 0. F
let a, b, c, d, e, h be Element of F; ( b <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F implies (d * c) - (h * e) = 0. F )
assume
b <> 0. F
; ( not (a * e) - (d * b) = 0. F or not (a * c) - (h * b) = 0. F or (d * c) - (h * e) = 0. F )
then
( (b * d) - (e * a) = 0. F & (b * h) - (c * a) = 0. F implies (e * h) - (c * d) = 0. F )
by Lm4;
hence
( not (a * e) - (d * b) = 0. F or not (a * c) - (h * b) = 0. F or (d * c) - (h * e) = 0. F )
by Lm5; verum