consider x being Element of C;
reconsider a = {x} as Element of Fin the carrier of C by FINSUB_1:def 5;
field the InternalRel of C = the carrier of C by ORDERS_1:97;
then ( the InternalRel of C is_reflexive_in the carrier of C & the InternalRel of C is_antisymmetric_in the carrier of C & the InternalRel of C is_transitive_in the carrier of C ) by RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
then A1: ( the InternalRel of C is_reflexive_in a & the InternalRel of C is_antisymmetric_in a & the InternalRel of C is_transitive_in a ) by ORDERS_1:93, ORDERS_1:94, ORDERS_1:95;
the InternalRel of C is_connected_in a

proof

let k, l be set ; :: according to RELAT_2:def 6 :: thesis: ( not k in a or not l in a or k = l or [k,l] in the InternalRel of C or [l,k] in the InternalRel of C )
assume A2: ( k in a & l in a & k <> l ) ; :: thesis: ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C )
then ( k = x & l = x ) by TARSKI:def 1;
hence ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) by A2; :: thesis: verum

end;

then the InternalRel of C linearly_orders a by A1, ORDERS_1:def 8;
then a in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ;
hence symplexes C is with_non-empty_element by SETFAM_1:def 11; :: thesis: verum