let T be non empty TopSpace; :: thesis: for O being open Subset of T
for A being Subset of T st O meets Cl A holds
O meets A
let O be open Subset of T; :: thesis: for A being Subset of T st O meets Cl A holds
O meets A
let A be Subset of T; :: 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:23;
then Cl A c= O ` by TOPS_1:5;
hence O misses Cl A by SUBSET_1:23; :: thesis: verum

end;

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