let x1, y1, x2, y2 be Real; :: thesis: [**x1,y1**] - [**x2,y2**] = [**(x1 - x2),(y1 - y2)**]
thus [**x1,y1**] - [**x2,y2**] = [**x1,y1**] + [**(- x2),(- y2)**] by Th5
.= [**(x1 - x2),(y1 - y2)**] ; :: thesis: verum