let C be non empty Poset; :: thesis: for x being Element of C holds {x} in symplexes C

let x be Element of C; :: thesis: {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

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

let x be Element of C; :: thesis: {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

A5:
field the InternalRel of C = the carrier of C
by ORDERS_1:12;
let k, l be object ; :: 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

A2: k in a and

A3: l in a and

A4: k <> l ; :: thesis: ( [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; :: thesis: verum

end;assume that

A2: k in a and

A3: l in a and

A4: k <> l ; :: thesis: ( [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; :: thesis: verum

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