let T be TopStruct ; :: thesis: bool the carrier of T is basis of T
reconsider P = bool the carrier of T as Subset-Family of T ;
reconsider P = P as Subset-Family of T ;
P is basis of T
proof
let p be Point of T; :: according to YELLOW13:def 4 :: thesis: P is basis of p
thus P is basis of p by Th18; :: thesis: verum
end;
hence bool the carrier of T is basis of T ; :: thesis: verum