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;