theorem Th12: :: EUCLID_3:12

for p being Point of (TOP-REAL 2) holds ((- p) `1) + (((- p) `2) * <i>) = (- (p `1)) + ((- (p `2)) * <i>)