let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds
( A is 1st_class iff UAp A c= LAp A )
let A be Subset of T; :: thesis: ( A is 1st_class iff UAp A c= LAp 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 1st_class iff UAp A c= LAp A ) by A2; :: thesis: verum