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