let C be non empty Poset; :: thesis: {} 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 ; :: thesis: verum

{} 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 ; :: thesis: verum