let C be non empty Poset; {} in symplexes C
{} is Subset of C
by SUBSET_1:1;
then reconsider a = {} as Element of Fin the carrier of C by FINSUB_1:def 5;
A1:
the InternalRel of C is_antisymmetric_in a
;
A2:
the InternalRel of C is_connected_in a
;
A3:
the InternalRel of C is_transitive_in a
;
the InternalRel of C is_reflexive_in a
;
then
the InternalRel of C linearly_orders a
by A1, A3, A2, ORDERS_1:def 9;
hence
{} in symplexes C
; verum