let T be non empty TopSpace; :: thesis: for x being Point of T
for y being Point of TopStruct(# the carrier of T, the topology of T #)
for A being set st x = y holds
( A is Basis of iff A is Basis of )
let x be Point of T; :: thesis: for y being Point of TopStruct(# the carrier of T, the topology of T #)
for A being set st x = y holds
( A is Basis of iff A is Basis of )
let y be Point of TopStruct(# the carrier of T, the topology of T #); :: thesis: for A being set st x = y holds
( A is Basis of iff A is Basis of )
let A be set ; :: thesis: ( x = y implies ( A is Basis of iff A is Basis of ) )
assume A1: x = y ; :: thesis: ( A is Basis of iff A is Basis of )
thus ( A is Basis of implies A is Basis of ) :: thesis: ( A is Basis of implies A is Basis of )

proof

assume A2: A is Basis of ; :: thesis: A is Basis of
then reconsider A = A as Subset-Family of TopStruct(# the carrier of T, the topology of T #) ;
A is Basis of

proof

A c= the topology of TopStruct(# the carrier of T, the topology of T #) by A2, TOPS_2:64;
then A3: A is open by TOPS_2:64;
A is y -quasi_basis by A1, A2, YELLOW_8:def 1, PRE_TOPC:30;
hence A is Basis of by A3; :: thesis: verum

end;

hence A is Basis of ; :: thesis: verum

end;

assume A4: A is Basis of ; :: thesis: A is Basis of
then reconsider A = A as Subset-Family of T ;
A is Basis of

proof

A c= the topology of T by A4, TOPS_2:64;
then A5: A is open by TOPS_2:64;
A is x -quasi_basis by A1, A4, YELLOW_8:def 1, PRE_TOPC:30;
hence A is Basis of by A5; :: thesis: verum

end;

hence A is Basis of ; :: thesis: verum