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