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