for t being Point of (TPlane (p,q)) holds pi_1 ((TPlane (p,q)),t) is trivial ;
hence TPlane (p,q) is having_trivial_Fundamental_Group by Def1; :: thesis: verum