consider p being Point of T;
set R = Indiscernibility T;
Class (Indiscernibility T),p in Class (Indiscernibility T) by EQREL_1:def 5;
hence Class (Indiscernibility T) is non empty a_partition of the carrier of T ; :: thesis: verum