theorem Th6: :: POLYNOM5:6
for x1, y1, x2, y2 being Real holds [**x1,y1**] - [**x2,y2**] = [**(x1 - x2),(y1 - y2)**]