x in Class the InternalRel of A,x by EQREL_1:28;
hence not card (Class the InternalRel of A,x) is empty ; :: thesis: verum