let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds
( A is 2nd_class iff LAp A c< UAp A )
let A be Subset of T; :: thesis: ( A is 2nd_class iff LAp A c< UAp A )
a2: LAp (UAp A) = UAp (UAp A) by ROUGHS_1:36
.= UAp A ;
UAp (LAp A) = LAp (LAp A) by ROUGHS_1:34
.= LAp A ;
hence ( A is 2nd_class iff LAp A c< UAp A ) by a2; :: thesis: verum