let R be Skew-Field; :: thesis: for s being set st s in the carrier of (MultGroup R) holds

s in the carrier of R

let s be set ; :: thesis: ( s in the carrier of (MultGroup R) implies s in the carrier of R )

assume s in the carrier of (MultGroup R) ; :: thesis: s in the carrier of R

then s in NonZero R by Def1;

hence s in the carrier of R ; :: thesis: verum

s in the carrier of R

let s be set ; :: thesis: ( s in the carrier of (MultGroup R) implies s in the carrier of R )

assume s in the carrier of (MultGroup R) ; :: thesis: s in the carrier of R

then s in NonZero R by Def1;

hence s in the carrier of R ; :: thesis: verum