let C be non empty Poset; :: thesis: {} in symplexes C
A1: {} is Subset of C by SUBSET_1:1;
then reconsider a = {} as Element of Fin the carrier of C by FINSUB_1:def 5;
A2: field the InternalRel of C = the carrier of C by ORDERS_1:12;
then the InternalRel of C is_antisymmetric_in the carrier of C by RELAT_2:def 12;
then A3: the InternalRel of C is_antisymmetric_in a by A1, ORDERS_1:9;
A4: 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 that
A5: k in a and
l in a and
k <> l ; :: thesis: ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C )
thus ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) by A5; :: thesis: verum

end;

the InternalRel of C is_transitive_in the carrier of C by A2, RELAT_2:def 16;
then A6: the InternalRel of C is_transitive_in a by A1, ORDERS_1:10;
the InternalRel of C is_reflexive_in the carrier of C by A2, RELAT_2:def 9;
then the InternalRel of C is_reflexive_in a by A1, ORDERS_1:8;
then the InternalRel of C linearly_orders a by A3, A6, A4, ORDERS_1:def 8;
hence {} in symplexes C ; :: thesis: verum