thus [x,y] is Point of [:X,Y:] by Def5; :: thesis: verum