let TS be TopSpace; :: thesis: for P being Subset of TS holds
( P is dense iff for Q being Subset of TS st Q <> {} & Q is open holds
P meets Q )
let P be Subset of TS; :: thesis: ( P is dense iff for Q being Subset of TS st Q <> {} & Q is open holds
P meets Q )

hereby :: thesis: ( ( for Q being Subset of TS st Q <> {} & Q is open holds
P meets Q ) implies P is dense )

assume A1: P is dense ; :: thesis: for Q being Subset of TS st Q <> {} & Q is open holds
P meets Q
let Q be Subset of TS; :: thesis: ( Q <> {} & Q is open implies P meets Q )
assume that
A2: Q <> {} and
A3: Q is open ; :: thesis: P meets Q
A4: Cl P = [#] TS by A1, Def3;
consider x being Element of Q;
x in Q by A2;
then A5: not TS is empty ;
x in Cl P by A2, A4, TARSKI:def 3;
hence P meets Q by A2, A3, A5, Th39; :: thesis: verum

end;

assume A6: for Q being Subset of TS st Q <> {} & Q is open holds
P meets Q ; :: thesis: P is dense
[#] TS c= Cl P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] TS or x in Cl P )
assume A7: x in [#] TS ; :: thesis: x in Cl P
then A8: not TS is empty ;
for C being Subset of TS st C is open & x in C holds
P meets C by A6;
hence x in Cl P by A7, A8, Th39; :: thesis: verum

end;

then Cl P = [#] TS by XBOOLE_0:def 10;
hence P is dense by Def3; :: thesis: verum