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