set x = the Element of C;
reconsider a = { the Element of C} 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 = the Element of C 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 ;
then a in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ;
hence not symplexes C is empty-membered by SETFAM_1:def 10; :: thesis: verum