let D be non empty set ; for p1, p2, p3 being Element of D st p1 <> p2 holds
Rotate (<*p1,p2,p3*>,p2) = <*p2,p3,p2*>
let p1, p2, p3 be Element of D; ( p1 <> p2 implies Rotate (<*p1,p2,p3*>,p2) = <*p2,p3,p2*> )
assume A1:
p1 <> p2
; Rotate (<*p1,p2,p3*>,p2) = <*p2,p3,p2*>
rng <*p1,p2,p3*> = {p1,p2,p3}
by Lm2;
then
p2 in rng <*p1,p2,p3*>
by ENUMSET1:def 1;
hence Rotate (<*p1,p2,p3*>,p2) =
(<*p1,p2,p3*> :- p2) ^ ((<*p1,p2,p3*> -: p2) /^ 1)
by Def2
.=
<*p2,p3*> ^ ((<*p1,p2,p3*> -: p2) /^ 1)
by A1, Th54
.=
<*p2,p3*> ^ (<*p1,p2*> /^ 1)
by A1, Th50
.=
<*p2,p3,p2*>
by Th46
;
verum