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 for U being Subset of T st U is open & p in U 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 for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} ) )
let p be Point of T; :: thesis: ( p in Fr A iff for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} ) )

hereby :: thesis: ( ( for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} ) ) implies p in Fr A )

assume A1: p in Fr A ; :: thesis: for U being Subset of T st U is open & p in U holds
( A meets U & U \ A <> {} )
let U be Subset of T; :: thesis: ( U is open & p in U implies ( A meets U & U \ A <> {} ) )
assume A2: ( U is open & p in U ) ; :: thesis: ( A meets U & U \ A <> {} )
then U meets A ` by A1, TOPS_1:28;
hence ( A meets U & U \ A <> {} ) by A1, A2, Th1, TOPS_1:28; :: thesis: verum

end;

assume A3: for U being Subset of T st U is open & p in U 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 A4: ( U is open & p in U ) ; :: thesis: ( A meets U & U meets A ` )
then U \ A <> {} by A3;
hence ( A meets U & U meets A ` ) by A3, A4, Th1; :: thesis: verum

end;

hence p in Fr A by TOPS_1:28; :: thesis: verum