assume A1: Rev p is trivial ; :: thesis: contradiction

per cases ( Rev p is empty or ex x being set st Rev p = <*x*> ) by A1, Th1;

suppose Rev p is empty ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose ex x being set st Rev p = <*x*> ; :: thesis: contradiction

then consider x being set such that
A2: Rev p = <*x*> ;
p = Rev <*x*> by A2, FINSEQ_6:29
.= <*x*> by FINSEQ_5:63 ;
hence contradiction ; :: thesis: verum

end;

end;