per cases ( x is real or not x is real ) ;
suppose x is real ; :: thesis: not x " is positive
then reconsider x = x as Real ;
not x " is positive ;
hence not x " is positive ; :: thesis: verum
end;
suppose not x is real ; :: thesis: not x " is positive
hence not x " is positive by Def6; :: thesis: verum
end;
end;