reconsider F = bool the carrier of T as Subset-Family of T ;
reconsider F = F as Subset-Family of T ;
take F ; :: thesis: for p being Point of T holds F is basis of p
thus for p being Point of T holds F is basis of p by Th18; :: thesis: verum