assume
A1
:
Rev
p
is
trivial
;
:: thesis:
contradiction
per
cases
(
Rev
p
is
empty
or ex
x
being
object
st
Rev
p
=
<*
x
*>
)
by
A1
,
Th1
;
suppose
Rev
p
is
empty
;
:: thesis:
contradiction
hence
contradiction ;
:: thesis:
verum
end;
suppose
ex
x
being
object
st
Rev
p
=
<*
x
*>
;
:: thesis:
contradiction
then
consider
x
being
object
such that
A2
:
Rev
p
=
<*
x
*>
;
p
=
Rev
<*
x
*>
by
A2
.=
<*
x
*>
by
FINSEQ_5:60
;
hence
contradiction ;
:: thesis:
verum
end;
end;