begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
definition
let X be
set ;
func PGraph X -> MultiGraphStruct equals
MultiGraphStruct(#
X,
[:X,X:],
(pr1 X,X),
(pr2 X,X) #);
coherence
MultiGraphStruct(# X,[:X,X:],(pr1 X,X),(pr2 X,X) #) is MultiGraphStruct
;
end;
:: deftheorem defines PGraph JGRAPH_1:def 1 :
theorem
canceled;
theorem
:: deftheorem Def2 defines PairF JGRAPH_1:def 2 :
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
begin
:: deftheorem Def3 defines is_Shortcut_of JGRAPH_1:def 3 :
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
:: deftheorem Def4 defines nodic JGRAPH_1:def 4 :
theorem
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
begin
theorem Th31:
for
a,
b,
r1,
r2 being
Real st
a <= r1 &
r1 <= b &
a <= r2 &
r2 <= b holds
abs (r1 - r2) <= b - a
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
begin
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem
canceled;
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem