let R be Skew-Field; :: thesis: the carrier of (MultGroup R) c= the carrier of R
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in the carrier of (MultGroup R) or 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