let T be non empty TopSpace; :: thesis: for O being open Subset of
for A being Subset of st O meets Cl A holds
O meets A
let O be open Subset of ; :: thesis: for A being Subset of st O meets Cl A holds
O meets A
let A be Subset of ; :: thesis: ( O meets Cl A implies O meets A )
( O misses A implies O misses Cl A )

proof

assume O misses A ; :: thesis: O misses Cl A
then A c= O ` by SUBSET_1:43;
then Cl A c= O ` by TOPS_1:31;
hence O misses Cl A by SUBSET_1:43; :: thesis: verum

end;

hence ( O meets Cl A implies O meets A ) ; :: thesis: verum