per cases ( p in rng f or not p in rng f ) ;
suppose A1: p in rng f ; :: thesis: not Rotate (f,p) is empty
not (f :- p) ^ ((f -: p) /^ 1) is empty ;
hence not Rotate (f,p) is empty by A1, Def2; :: thesis: verum
end;
suppose not p in rng f ; :: thesis: not Rotate (f,p) is empty
hence not Rotate (f,p) is empty by Def2; :: thesis: verum
end;
end;