per
cases
(
p
in
rng
f
or not
p
in
rng
f
)
;
suppose
A1
:
p
in
rng
f
;
:: thesis:
not
Rotate
(
f
,
p
) is
empty
not
(
f
:-
p
)
^
(
(
f
-:
p
)
/^
1
)
is
empty
;
hence
not
Rotate
(
f
,
p
) is
empty
by
A1
,
Def2
;
:: thesis:
verum
end;
suppose
not
p
in
rng
f
;
:: thesis:
not
Rotate
(
f
,
p
) is
empty
hence
not
Rotate
(
f
,
p
) is
empty
by
Def2
;
:: thesis:
verum
end;
end;