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;