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 P is dense ; :: thesis: for Q being Subset of TS st Q <> {} & Q is open holds
P meets Q
then A1: Cl P = [#] TS ;
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
set x = the Element of Q;
the Element of Q in Q by A2;
then A4: not TS is empty ;
the Element of Q in Cl P by A2, A1, TARSKI:def 3;
hence P meets Q by A2, A3, A4, Th12; :: thesis: verum

end;

assume A5: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] TS or x in Cl P )
A6: for C being Subset of TS st C is open & x in C holds
P meets C by A5;
assume A7: x in [#] TS ; :: thesis: x in Cl P
then not TS is empty ;
hence x in Cl P by A7, A6, Th12; :: thesis: verum

end;

then Cl P = [#] TS ;
hence P is dense ; :: thesis: verum