let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds UAp A = Cl A
let A be Subset of T; :: thesis: UAp A = Cl A
UAp A c= Cl A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp A or x in Cl A )
assume A1: x in UAp A ; :: thesis: x in Cl A
then reconsider xx = x as set ;
for C being Subset of T st C is closed & A c= C holds
xx in C

proof

let C be Subset of T; :: thesis: ( C is closed & A c= C implies xx in C )
assume C is closed ; :: thesis: ( not A c= C or xx in C )
then B3: UAp C = C by UApCl1;
assume A c= C ; :: thesis: xx in C
then UAp A c= UAp C by ROUGHS_1:25;
hence xx in C by B3, A1; :: thesis: verum

end;

hence x in Cl A by PRE_TOPC:15, A1; :: thesis: verum

end;

hence UAp A = Cl A by TOPS_1:5, ROUGHS_1:13; :: thesis: verum