let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being open Subset of T holds LAp A = Int A
let A be open Subset of T; :: thesis: LAp A = Int A
Int A = A by TOPS_1:23;
hence LAp A = Int A by OpIsLap; :: thesis: verum