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

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