let C be non empty Poset; :: thesis: {} in symplexes C
A1: {} is Subset of C by SUBSET_1:4;
then reconsider a = {} 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 A2: ( 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 A1, 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 ( k in a & l in a & k <> l ) ; :: thesis: ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C )
hence ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) ; :: thesis: verum

end;

then the InternalRel of C linearly_orders a by A2, ORDERS_1:def 8;
hence {} in symplexes C ; :: thesis: verum