let F be Field; :: thesis: for K, L, R being Element of F holds (K - L) - (R - L) = K - R
let K, L, R be Element of F; :: thesis: (K - L) - (R - L) = K - R
thus (K - L) - (R - L) = (K + (- L)) - (R - L) by RLVECT_1:def 11
.= ((- L) + K) - (R + (- L)) by RLVECT_1:def 11
.= K - R by Lm4 ; :: thesis: verum