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