let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds not A is 3rd_class
let A be Subset of T; :: thesis: not A is 3rd_class
A1: ( A is 3rd_class iff Cl (Int A), Int (Cl A) are_c=-incomparable ) ;
LAp (UAp A) = UAp (UAp A) by ROUGHS_1:36
.= UAp A ;
hence not A is 3rd_class by ROUGHS_1:25, ROUGHS_1:12, A1; :: thesis: verum