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