the carrier of (pi_1 X,a) = Class (EqRel X,a) by Def3;
hence not the carrier of (pi_1 X,a) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum