set
W
=
G
.walkOf
(
x
,
e
,
x
);
now
:: thesis:
G
.walkOf
(
x
,
e
,
x
) is
closed
per
cases
(
e
Joins
x
,
x
,
G
or not
e
Joins
x
,
x
,
G
)
;
suppose
A1
:
e
Joins
x
,
x
,
G
;
:: thesis:
G
.walkOf
(
x
,
e
,
x
) is
closed
then
A2
:
(
G
.walkOf
(
x
,
e
,
x
))
.last()
=
x
by
Lm6
;
(
G
.walkOf
(
x
,
e
,
x
))
.first()
=
x
by
A1
,
Lm6
;
hence
G
.walkOf
(
x
,
e
,
x
) is
closed
by
A2
;
:: thesis:
verum
end;
suppose
not
e
Joins
x
,
x
,
G
;
:: thesis:
G
.walkOf
(
x
,
e
,
x
) is
closed
then
G
.walkOf
(
x
,
e
,
x
)
=
G
.walkOf
the
Element
of
the_Vertices_of
G
by
Def5
;
hence
G
.walkOf
(
x
,
e
,
x
) is
closed
;
:: thesis:
verum
end;
end;
end;
hence
G
.walkOf
(
x
,
e
,
x
) is
closed
;
:: thesis:
verum