take T = the non empty with_equivalence naturally_generated TopRelStr ; :: thesis: T is without_3rd_class_subsets
thus T is without_3rd_class_subsets ; :: thesis: verum