let V be RealLinearSpace; :: thesis: for P, Q, R, S being Element of V
for r being Real st P - Q = r * (R - S) holds
Q - P = r * (S - R)
let P, Q, R, S be Element of V; :: thesis: for r being Real st P - Q = r * (R - S) holds
Q - P = r * (S - R)
let r be Real; :: thesis: ( P - Q = r * (R - S) implies Q - P = r * (S - R) )
assume A1: P - Q = r * (R - S) ; :: thesis: Q - P = r * (S - R)
Q - P = - (r * (R - S)) by A1, RLVECT_1:33
.= r * (- (R - S)) by RLVECT_1:25
.= r * (S - R) by RLVECT_1:33 ;
hence Q - P = r * (S - R) ; :: thesis: verum