let a be Point of T; :: thesis: a,a are_connected
thus a,a are_connected ; :: thesis: verum