let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds
( A is 1st_class iff A is exact )
let A be Subset of T; :: thesis: ( A is 1st_class iff A is exact )
thus ( A is 1st_class implies A is exact ) :: thesis: ( A is exact implies A is 1st_class )
proof
assume A is 1st_class ; :: thesis: A is exact
then LAp A = UAp A by ROUGHS_1:14, FirstApprox;
then LAp A = A by ROUGHS_1:13, ROUGHS_1:12;
hence A is exact ; :: thesis: verum
end;
assume A is exact ; :: thesis: A is 1st_class
hence A is 1st_class by ROUGHS_1:16; :: thesis: verum