consider B being Basis of T;
deffunc H₁( Point of ) -> set = { U where U is Subset of : ( $1 in U & U in B ) } ;
consider F being ManySortedSet of T such that
A1: for x being Point of holds F . x = H₁(x) from PBOOLE:sch 5();
take F ; :: thesis: for x being Element of holds F . x is Basis of x
let x be Point of ; :: thesis: F . x is Basis of x
F . x = H₁(x) by A1;
hence F . x is Basis of x by Th1; :: thesis: verum