let D be non empty set ; :: thesis: for p1, p2, p3 being Element of D st p2 <> p3 holds
Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*>
let p1, p2, p3 be Element of D; :: thesis: ( p2 <> p3 implies Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*> )
assume A1: p2 <> p3 ; :: thesis: Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*>

per cases ( p1 = p3 or p1 <> p3 ) ;

suppose p1 = p3 ; :: thesis: Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*>

hence Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*> by Th97; :: thesis: verum

end;

suppose A2: p1 <> p3 ; :: thesis: Rotate (<*p1,p2,p3*>,p3) = <*p3,p2,p3*>

rng <*p1,p2,p3*> = {p1,p2,p3} by Lm2;
then p3 in rng <*p1,p2,p3*> by ENUMSET1:def 1;
hence Rotate (<*p1,p2,p3*>,p3) = (<*p1,p2,p3*> :- p3) ^ ((<*p1,p2,p3*> -: p3) /^ 1) by Def2
.= <*p3*> ^ ((<*p1,p2,p3*> -: p3) /^ 1) by A1, A2, Th55
.= <*p3*> ^ (<*p1,p2,p3*> /^ 1) by A1, A2, Th51
.= <*p3*> ^ <*p2,p3*> by Th47
.= <*p3,p2,p3*> by FINSEQ_1:43 ;
:: thesis: verum

end;

end;