let a, b be Real; :: thesis: ( b <> 0 implies ex c being Real st a = b / c )
assume A1: b <> 0 ; :: thesis: ex c being Real st a = b / c
then consider c being Complex such that
A2: a = b / c by XCMPLX_1:232;

per cases ( c = 0 or c <> 0 ) ;

suppose c = 0 ; :: thesis: ex c being Real st a = b / c

hence ex c being Real st a = b / c by A2; :: thesis: verum

end;

suppose c <> 0 ; :: thesis: ex c being Real st a = b / c

then c = b / a by A1, A2, XCMPLX_1:54;
then reconsider c = c as Real ;
take c ; :: thesis: a = b / c
thus a = b / c by A2; :: thesis: verum

end;

end;