begin
theorem
:: deftheorem Def1 defines maxPrefix HELLY:def 1 :
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
begin
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem Th24:
begin
theorem Th25:
theorem Th26:
theorem Th27:
:: deftheorem Def2 defines .pathBetween HELLY:def 2 :
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
Lm1:
for T being _Tree
for a, b, c being Vertex of 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
for P1, P4 being Path of non empty 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 ;
func MiddleVertex a,
b,
c -> Vertex of
means :
Def3:
(((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {it};
existence
ex b1 being Vertex of st (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {b1}
uniqueness
for b1, b2 being Vertex of 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:6;
end;
:: deftheorem Def3 defines MiddleVertex HELLY:def 3 :
theorem Th41:
theorem Th42:
theorem
theorem Th44:
theorem
theorem Th46:
theorem
theorem Th48:
theorem Th49:
theorem
theorem Th51:
theorem
for
T being
_Tree for
P1,
P2,
P3,
P4 being
Path of non
empty for
a,
b,
c being
Vertex of 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))
theorem Th53:
begin
:: deftheorem defines with_Helly_property HELLY:def 4 :
theorem