set
W
=
G
.walkOf
(
x
,
e
,
y
);
now
:: thesis:
G
.walkOf
(
x
,
e
,
y
) is
Path-like
per
cases
(
e
Joins
x
,
y
,
G
or not
e
Joins
x
,
y
,
G
)
;
suppose
e
Joins
x
,
y
,
G
;
:: thesis:
G
.walkOf
(
x
,
e
,
y
) is
Path-like
hence
G
.walkOf
(
x
,
e
,
y
) is
Path-like
by
Lm62
;
:: thesis:
verum
end;
suppose
not
e
Joins
x
,
y
,
G
;
:: thesis:
G
.walkOf
(
x
,
e
,
y
) is
Path-like
then
G
.walkOf
(
x
,
e
,
y
)
=
G
.walkOf
the
Element
of
the_Vertices_of
G
by
Def5
;
hence
G
.walkOf
(
x
,
e
,
y
) is
Path-like
;
:: thesis:
verum
end;
end;
end;
hence
G
.walkOf
(
x
,
e
,
y
) is
Path-like
;
:: thesis:
verum