theorem :: ROUGHS_4:13

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds
( A is 1st_class iff LAp (UAp A) c= UAp (LAp A) ) ;