now :: thesis: not 0 in Inv X

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

end;

hence Inv X is without_zero ; :: thesis: verum