let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds BndAp A = Fr A
let A be Subset of T; :: thesis: BndAp A = Fr A
( UAp A = Cl A & Int A = LAp A ) by UApCl, LApInt;
hence BndAp A = Fr A ; :: thesis: verum