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;