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

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;

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

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

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 = the Element of C 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 = the Element of C 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;

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