now

assume 0 in Inv X ; :: thesis: contradiction
then ex r3 being Real st
( 0 = 1 / r3 & r3 in X ) ;
hence contradiction by XCMPLX_1:203; :: thesis: verum

end;

hence Inv X is without_zero by Def1; :: thesis: verum