let T be non empty TopSpace; :: thesis:
let A be Subset of T; :: thesis:
let p be Point of T; :: thesis:

end;

assume A3: for U being open Subset of T st p in U holds
ex q being Point of T st
( q <> p & q in A & q in U ) ; :: thesis:
for U being open Subset of T st p in U holds
ex y being Point of T st
( y in A /\ U & p <> y )

let U be open Subset of T; :: thesis:
assume p in U ; :: thesis:
then consider q being Point of T such that
A4: ( q <> p & q in A & q in U ) by A3;
take q ; :: thesis:
thus ( q in A /\ U & p <> q ) by A4, XBOOLE_0:def 4; :: thesis:

end;