let T be non empty anti-discrete TopStruct ; :: thesis: for p being Point of T holds { the carrier of T} is correct basis of p
let p be Point of T; :: thesis: { the carrier of T} is correct basis of p
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 ;
reconsider A = A as Subset-Family of T ;
A is basis of p
proof
let S be a_neighborhood of p; :: according to YELLOW13:def 2 :: thesis: ex P being a_neighborhood of p st
( P in A & P c= S )
take S ; :: thesis: ( S in A & S c= S )
p in Int S by CONNSP_2:def 1;
then A2: Int S = the carrier of T by TDLAT_3:18;
Int S c= S by TOPS_1:16;
then Int S = S by A2;
hence ( S in A & S c= S ) by A2, TARSKI:def 1; :: thesis: verum
end;
then reconsider A = A as basis of p ;
A is correct
proof
let X be Subset of T; :: according to YELLOW13:def 3 :: thesis: ( X in A iff p in Int X )
hereby :: thesis: ( p in Int X implies X in A )
assume X in A ; :: thesis: p in Int X
then X = the carrier of T by TARSKI:def 1;
then Int X = [#] T by TOPS_1:15;
hence p in Int X ; :: thesis: verum
end;
assume p in Int X ; :: thesis: X in A
then A3: Int X = the carrier of T by TDLAT_3:18;
Int X c= X by TOPS_1:16;
then Int X = X by A3;
hence X in A by A3, TARSKI:def 1; :: thesis: verum
end;
hence { the carrier of T} is correct basis of p ; :: thesis: verum