theorem FirstApprox: :: ROUGHS_4:14

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