let V be RealNormSpace; :: thesis: for x being Point of V
for y being Point of (DualSp V) holds (- x) .|. (- y) = x .|. y
let x be Point of V; :: thesis: for y being Point of (DualSp V) holds (- x) .|. (- y) = x .|. y
let y be Point of (DualSp V); :: thesis: (- x) .|. (- y) = x .|. y
thus (- x) .|. (- y) = - (x .|. (- y)) by Th10
.= - (- (x .|. y)) by Th9
.= x .|. y ; :: thesis: verum