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
proof
thus y in Intersect A by A1, A2, YELLOW_8:def 1; :: according to YELLOW_8:def 1 :: 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
A4: S is open and
A5: 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 A4, PRE_TOPC:30;
then consider W being Subset of T such that
A6: ( W in A & W c= SS ) by A1, A2, A5, YELLOW_8:def 1;
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 A6; :: thesis: verum
end;
hence A is Basis of by A3; :: thesis: verum
end;
hence A is Basis of ; :: thesis: verum
end;
assume A7: 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 A7, TOPS_2:64;
then A8: A is open by TOPS_2:64;
A is x -quasi_basis
proof
thus x in Intersect A by A1, A7, YELLOW_8:def 1; :: according to YELLOW_8:def 1 :: 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
A9: S is open and
A10: 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 A9, PRE_TOPC:30;
then consider W being Subset of TopStruct(# the carrier of T, the topology of T #) such that
A11: ( W in A & W c= SS ) by A1, A7, A10, YELLOW_8:def 1;
reconsider V = W as Subset of T ;
take V ; :: thesis: ( V in A & V c= S )
thus ( V in A & V c= S ) by A11; :: thesis: verum
end;
hence A is Basis of by A8; :: thesis: verum
end;
hence A is Basis of ; :: thesis: verum