let C be non empty Poset; :: thesis: for x being Element of C holds {x} in symplexes C
let x be Element of C; :: thesis: {x} in symplexes 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;
hence {x} in symplexes C ; :: thesis: verum