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

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

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

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

end;

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

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

end;

end;