let R be Skew-Field; :: thesis: NonZero R = units R
for x being object st x in NonZero R holds
x in units R

proof

let x be object ; :: thesis: ( x in NonZero R implies x in units R )
assume A1: x in NonZero R ; :: thesis: x in units R
then reconsider X = x as Element of R ;
X <> 0. R by A1, STRUCT_0:1;
then consider Y being Element of R such that
A2: Y * X = 1. R by ALGSTR_0:def 27, ALGSTR_0:def 39;
X * Y = 1. R by A2, VECTSP_2:7;
then X is unital by A2, GCD_1:def 2;
hence x in units R ; :: thesis: verum

end;

then A3: NonZero R c= units R by TARSKI:def 3;
for x being object st x in units R holds
x in NonZero R

proof

let x be object ; :: thesis: ( x in units R implies x in NonZero R )
assume A4: x in units R ; :: thesis: x in NonZero R
then reconsider X = x as Element of R ;
consider Y being Element of R such that
A5: ( X * Y = 1. R & Y * X = 1. R ) by A4, Th107, GCD_1:def 2;
( X <> 0. R & Y <> 0. R ) by A5;
hence x in NonZero R by STRUCT_0:1, STRUCT_0:def 12; :: thesis: verum

end;

then units R c= NonZero R by TARSKI:def 3;
hence NonZero R = units R by A3, XBOOLE_0:def 10; :: thesis: verum