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 )

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

hence
( O meets Cl A implies O meets A )
; :: thesis: verum
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;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