the carrier of (R / I) = Class (EqRel (R,I)) by Def6;
hence not the carrier of (R / I) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum