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 ;
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 = 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;
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;
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; verum