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