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