let h be Automorphism of S; :: thesis: ( h is id R -extending implies h is R -fixing )
assume h is id R -extending ; :: thesis: h is R -fixing
then h | R = id R by e1;
hence h is R -fixing by e0; :: thesis: verum