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;