let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds
( A is closed iff UAp A = A )
let A be Subset of T; :: thesis: ( A is closed iff UAp A = A )
thus ( A is closed implies UAp A = A ) :: thesis: ( UAp A = A implies A is closed )
proof
assume A is closed ; :: thesis: UAp A = A
then Z: (LAp (A `)) ` = (A `) ` by OpIsLap;
(LAp (A `)) ` = ((UAp A) `) ` by ROUGHS_1:28
.= UAp A ;
hence UAp A = A by Z; :: thesis: verum
end;
assume Z1: UAp A = A ; :: thesis: A is closed
(LAp (A `)) ` = ((UAp A) `) ` by ROUGHS_1:28
.= UAp A ;
hence A is closed by Z1; :: thesis: verum