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 x iff A is Basis of y )
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 x iff A is Basis of y )
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 x iff A is Basis of y )
let A be set ; :: thesis: ( x = y implies ( A is Basis of x iff A is Basis of y ) )
assume A1: x = y ; :: thesis: ( A is Basis of x iff A is Basis of y )
thus ( A is Basis of x implies A is Basis of y ) :: thesis: ( A is Basis of y implies A is Basis of x )
proof
assume A2: A is Basis of x ; :: thesis: A is Basis of y
then reconsider A = A as Subset-Family of TopStruct(# the carrier of T,the topology of T #) ;
A is Basis of y
proof
A c= the topology of TopStruct(# the carrier of T,the topology of T #) by A2, TOPS_2:78;
then A10: A is open by TOPS_2:78;
A is y -quasi_basis
proof
thus y in Intersect A by A1, A2, YELLOW_8:def 2; :: according to YELLOW_8:def 2 :: thesis: for b1 being Element of bool the carrier of TopStruct(# the carrier of T,the topology of T #) holds
( not b1 is open or not y in b1 or ex b2 being Element of bool the carrier of TopStruct(# the carrier of T,the topology of T #) st
( b2 in A & b2 c= b1 ) )
let S be Subset of TopStruct(# the carrier of T,the topology of T #); :: thesis: ( not S is open or not y in S or ex b1 being Element of bool the carrier of TopStruct(# the carrier of T,the topology of T #) st
( b1 in A & b1 c= S ) )
reconsider SS = S as Subset of T ;
assume that
A3: S is open and
A4: y in S ; :: thesis: ex b1 being Element of bool the carrier of TopStruct(# the carrier of T,the topology of T #) st
( b1 in A & b1 c= S )
SS is open by A3, PRE_TOPC:60;
then consider W being Subset of T such that
A5: ( W in A & W c= SS ) by A1, A2, A4, YELLOW_8:def 2;
reconsider V = W as Subset of TopStruct(# the carrier of T,the topology of T #) ;
take V ; :: thesis: ( V in A & V c= S )
thus ( V in A & V c= S ) by A5; :: thesis: verum
end;
hence A is Basis of y by A10; :: thesis: verum
end;
hence A is Basis of y ; :: thesis: verum
end;
assume A6: A is Basis of y ; :: thesis: A is Basis of x
then reconsider A = A as Subset-Family of T ;
A is Basis of x
proof
A c= the topology of T by A6, TOPS_2:78, YELLOW_8:def 2;
then A10: A is open by A6, TOPS_2:78, YELLOW_8:def 2;
A is x -quasi_basis
proof
thus x in Intersect A by A1, A6, YELLOW_8:def 2; :: according to YELLOW_8:def 2 :: thesis: for b1 being Element of bool the carrier of T holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of T st
( b2 in A & b2 c= b1 ) )
let S be Subset of T; :: thesis: ( not S is open or not x in S or ex b1 being Element of bool the carrier of T st
( b1 in A & b1 c= S ) )
reconsider SS = S as Subset of TopStruct(# the carrier of T,the topology of T #) ;
assume that
A7: S is open and
A8: x in S ; :: thesis: ex b1 being Element of bool the carrier of T st
( b1 in A & b1 c= S )
SS is open by A7, PRE_TOPC:60;
then consider W being Subset of TopStruct(# the carrier of T,the topology of T #) such that
A9: ( W in A & W c= SS ) by A1, A6, A8, YELLOW_8:def 2;
reconsider V = W as Subset of T ;
take V ; :: thesis: ( V in A & V c= S )
thus ( V in A & V c= S ) by A9; :: thesis: verum
end;
hence A is Basis of x by A10; :: thesis: verum
end;
hence A is Basis of x ; :: thesis: verum