let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds LAp A = Int A
let A be Subset of T; :: thesis: LAp A = Int A
Int A c= LAp A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Int A or x in LAp A )
assume A1: x in Int A ; :: thesis: x in LAp A
then reconsider xx = x as set ;
consider Q being Subset of T such that
A2: ( Q is open & Q c= A & xx in Q ) by TOPS_1:22, A1;
Q = Int Q by A2, TOPS_1:23;
then A3: Q = LAp Q by OpenLap;
LAp Q c= LAp A by A2, ROUGHS_1:24;
hence x in LAp A by A2, A3; :: thesis: verum
end;
hence LAp A = Int A by TOPS_1:24, ROUGHS_1:12; :: thesis: verum