let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds
( A is 2nd_class iff A is rough )
let A be Subset of T; :: thesis: ( A is 2nd_class iff A is rough )
thus ( A is 2nd_class implies A is rough ) ; :: thesis: ( A is rough implies A is 2nd_class )
assume C1: A is rough ; :: thesis: A is 2nd_class
LAp A <> UAp A

proof

assume LAp A = UAp A ; :: thesis: contradiction
then LAp A = A by ROUGHS_1:13, ROUGHS_1:12;
hence contradiction by C1; :: thesis: verum

end;

then LAp A c< UAp A by ROUGHS_1:14;
hence A is 2nd_class by SecondClass; :: thesis: verum