environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FINSEQ_1, FUNCT_1, GRAPH_2, ARYTM_3, NAT_1, XXREAL_0, SUBSET_1, TREES_1, TARSKI, CARD_1, ORDINAL1, FINSET_1, MEMBERED, RELAT_1, ORDINAL4, GLIB_000, GLIB_001, ABIAN, ZFMISC_1, ARYTM_1, GRAPH_1, RCOMP_1, SETFAM_1, HELLY;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, SETFAM_1, FUNCT_1, FINSEQ_1, MEMBERED, NAT_1, TREES_1, XXREAL_2, ABIAN, GRAPH_2, GLIB_000, GLIB_001, GLIB_002;
definitions TARSKI, XBOOLE_0, GLIB_001;
theorems TARSKI, NAT_1, SETFAM_1, XBOOLE_0, XBOOLE_1, GRFUNC_1, FUNCT_1, ZFMISC_1, ORDINAL1, FINSEQ_1, FINSEQ_2, FINSEQ_3, INT_1, EULER_1, CARD_1, XREAL_1, XXREAL_0, CHORD, ABIAN, GLIB_000, GLIB_001, GLIB_002, MSSCYC_1, MEMBERED, GRAPH_2, XXREAL_2, FINSEQ_4, PRE_CIRC;
schemes NAT_1, FINSEQ_1;
registrations FINSET_1, XREAL_0, XXREAL_0, NAT_1, INT_1, RELAT_1, FINSEQ_1, ABIAN, MEMBERED, GLIB_000, GLIB_001, GLIB_002, XXREAL_2, CARD_1, FUNCT_1, XBOOLE_0, ORDINAL1;
constructors HIDDEN, DOMAIN_1, SETFAM_1, NAT_1, GRAPH_2, GLIB_001, GLIB_002, XXREAL_2, RELSET_1, RAT_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities GLIB_001;
expansions TARSKI, XBOOLE_0, GLIB_001;
Lm1:
for T being _Tree
for a, b, c being Vertex of T st c in (T .pathBetween (a,b)) .vertices() holds
(((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c}
Lm2:
for T being _Tree
for a, b, c being Vertex of T
for P1, P4 being Path of T st P1 = T .pathBetween (a,b) & P4 = T .pathBetween (a,c) & not P1 c= P4 & not P4 c= P1 holds
((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))}
definition
let T be
_Tree;
let a,
b,
c be
Vertex of
T;
existence
ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1}
uniqueness
for b1, b2 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} & (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b2} holds
b1 = b2
by ZFMISC_1:3;
end;
theorem
for
T being
_Tree for
P1,
P2,
P3,
P4 being
Path of
T for
a,
b,
c being
Vertex of
T st
P1 = T .pathBetween (
a,
b) &
P2 = T .pathBetween (
a,
c) &
P3 = T .pathBetween (
b,
a) &
P4 = T .pathBetween (
b,
c) & not
b in P2 .vertices() & not
c in P1 .vertices() & not
a in P4 .vertices() holds
P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4)))