let T be TopStruct ; :: thesis: for p being Point of T holds bool the carrier of T is basis of p
let p be Point of T; :: thesis: bool the carrier of T is basis of p
reconsider F = bool the carrier of T as Subset-Family of T ;
reconsider F = F as Subset-Family of T ;
F is basis of p

proof

let A be Subset of T; :: according to YELLOW13:def 1 :: thesis: ( p in Int A implies ex P being Subset of T st
( P in F & p in Int P & P c= A ) )
assume A1: p in Int A ; :: thesis: ex P being Subset of T st
( P in F & p in Int P & P c= A )
take Int A ; :: thesis: ( Int A in F & p in Int (Int A) & Int A c= A )
thus ( Int A in F & p in Int (Int A) & Int A c= A ) by A1, TOPS_1:16; :: thesis: verum

end;

hence bool the carrier of T is basis of p ; :: thesis: verum