for x being Point of T holds N . x is Basis of x by Def3;
hence Union N is Basis of T by Th2; :: thesis: verum