let C be non empty Poset; for x being Element of C holds {x} in symplexes C
let x be Element of C; {x} in symplexes C
reconsider a = {x} as Element of Fin the carrier of C by FINSUB_1:def 5;
A1:
the InternalRel of C is_connected_in a
proof
let k,
l be
object ;
RELAT_2:def 6 ( 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 A2:
k in a
and A3:
l in a
and A4:
k <> l
;
( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C )
k = x
by A2, TARSKI:def 1;
hence
(
[k,l] in the
InternalRel of
C or
[l,k] in the
InternalRel of
C )
by A3, A4, TARSKI:def 1;
verum
end;
A5:
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 A6:
the InternalRel of C is_antisymmetric_in a
;
the InternalRel of C is_transitive_in the carrier of C
by A5, RELAT_2:def 16;
then A7:
the InternalRel of C is_transitive_in a
;
the InternalRel of C is_reflexive_in the carrier of C
by A5, RELAT_2:def 9;
then
the InternalRel of C is_reflexive_in a
;
then
the InternalRel of C linearly_orders a
by A6, A7, A1, ORDERS_1:def 9;
hence
{x} in symplexes C
; verum