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:
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 ; :: 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 ;
hence ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) by ; :: thesis: 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 ;
then A7: the InternalRel of C is_transitive_in a ;
the InternalRel of C is_reflexive_in the carrier of C by ;
then the InternalRel of C is_reflexive_in a ;
then the InternalRel of C linearly_orders a by ;
hence {x} in symplexes C ; :: thesis: verum