let X be RealUnitarySpace; :: thesis: for x, y, z being Point of X holds x .|. (y - z) = (x .|. y) - (x .|. z)
let x, y, z be Point of X; :: thesis: x .|. (y - z) = (x .|. y) - (x .|. z)
x .|. (y - z) = (x .|. y) + (x .|. (- z)) by Def2
.= (x .|. y) + (- (x .|. z)) by Th8 ;
hence x .|. (y - z) = (x .|. y) - (x .|. z) ; :: thesis: verum