let T be non empty anti-discrete TopStruct ; :: thesis: for p being Point of T holds { the carrier of T} is Basis of
let p be Point of T; :: thesis: { the carrier of T} is Basis of
set A = { the carrier of T};
{ the carrier of T} c= bool the carrier of T

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { the carrier of T} or a in bool the carrier of T )
assume a in { the carrier of T} ; :: thesis: a in bool the carrier of T
then A1: a = the carrier of T by TARSKI:def 1;
the carrier of T c= the carrier of T ;
hence a in bool the carrier of T by A1; :: thesis: verum

end;

then reconsider A = { the carrier of T} as Subset-Family of T ;
A is Basis of

proof

A2: A is open

proof

let a be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not a in A or a is open )
assume a in A ; :: thesis: a is open
then a = [#] T by TARSKI:def 1;
hence a is open ; :: thesis: verum

end;

A is p -quasi_basis

proof

Intersect A = meet A by SETFAM_1:def 9
.= the carrier of T by SETFAM_1:10 ;
hence p in Intersect A ; :: according to YELLOW_8:def 1 :: thesis: for b₁ being Element of bool the carrier of T holds
( not b₁ is open or not p in b₁ or ex b₂ being Element of bool the carrier of T st
( b₂ in A & b₂ c= b₁ ) )
let S be Subset of T; :: thesis: ( not S is open or not p in S or ex b₁ being Element of bool the carrier of T st
( b₁ in A & b₁ c= S ) )
assume ( S is open & p in S ) ; :: thesis: ex b₁ being Element of bool the carrier of T st
( b₁ in A & b₁ c= S )
then A3: S = the carrier of T by TDLAT_3:18;
take S ; :: thesis: ( S in A & S c= S )
thus ( S in A & S c= S ) by A3, TARSKI:def 1; :: thesis: verum

end;

hence A is Basis of by A2; :: thesis: verum

end;

hence { the carrier of T} is Basis of ; :: thesis: verum