let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( A is dense iff for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) )
let A be Subset of X; :: thesis: ( A is dense iff for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) )
thus ( A is dense implies for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) ) :: thesis: ( ( for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) ) implies A is dense )
proof
assume A1: A is dense ; :: thesis: for G being Subset of X st G is open holds
Cl G = Cl (G /\ A)
let G be Subset of X; :: thesis: ( G is open implies Cl G = Cl (G /\ A) )
assume G is open ; :: thesis: Cl G = Cl (G /\ A)
then A2: Cl (G /\ (Cl A)) = Cl (G /\ A) by TOPS_1:14;
G /\ ([#] X) = G by XBOOLE_1:28;
hence Cl G = Cl (G /\ A) by A1, A2; :: thesis: verum
end;
assume for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) ; :: thesis: A is dense
then Cl ([#] X) = Cl (([#] X) /\ A) ;
then A3: [#] X = Cl (([#] X) /\ A) by TOPS_1:2;
([#] X) /\ A = A by XBOOLE_1:28;
hence A is dense by A3; :: thesis: verum