let T be non empty TopSpace; :: thesis: for A being Subset of T
for p being Point of T holds
( p in Fr A iff ex B being Basis of st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )
let A be Subset of T; :: thesis: for p being Point of T holds
( p in Fr A iff ex B being Basis of st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )
let p be Point of T; :: thesis: ( p in Fr A iff ex B being Basis of st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) )
hereby :: thesis: ( ex B being Basis of st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) implies p in Fr A )
set B = the Basis of ;
assume A1: p in Fr A ; :: thesis: ex B being Basis of st
for U being Subset of T st U in B holds
( A meets U & U \ A <> {} )
take B = the Basis of ; :: thesis: for U being Subset of T st U in B holds
( A meets U & U \ A <> {} )
let U be Subset of T; :: thesis: ( U in B implies ( A meets U & U \ A <> {} ) )
assume U in B ; :: thesis: ( A meets U & U \ A <> {} )
then ( U is open & p in U ) by YELLOW_8:12;
hence ( A meets U & U \ A <> {} ) by A1, Th9; :: thesis: verum
end;
given B being Basis of such that A2: for U being Subset of T st U in B holds
( A meets U & U \ A <> {} ) ; :: thesis: p in Fr A
for U being Subset of T st U is open & p in U holds
( A meets U & U meets A ` )
proof
let U be Subset of T; :: thesis: ( U is open & p in U implies ( A meets U & U meets A ` ) )
assume ( U is open & p in U ) ; :: thesis: ( A meets U & U meets A ` )
then consider V being Subset of T such that
A3: V in B and
A4: V c= U by YELLOW_8:def 1;
V \ A <> {} by A2, A3;
then A5: U \ A <> {} by A4, XBOOLE_1:3, XBOOLE_1:33;
A meets V by A2, A3;
hence ( A meets U & U meets A ` ) by A4, A5, Th1, XBOOLE_1:63; :: thesis: verum
end;
hence p in Fr A by TOPS_1:28; :: thesis: verum