let V be RealLinearSpace; :: thesis: ( V is non trivial RealLinearSpace iff ex u being Element of V st u in NonZero V )
A1: ( V is non trivial RealLinearSpace implies ex u being Element of V st u in NonZero V )

proof

assume V is non trivial RealLinearSpace ; :: thesis: ex u being Element of V st u in NonZero V
then consider u being Element of V such that
A2: u <> 0. V by STRUCT_0:def 19;
reconsider u = u as Element of V ;
take u ; :: thesis: u in NonZero V
( u in NonZero V iff not u is zero ) by STRUCT_0:1;
hence u in NonZero V by A2, STRUCT_0:def 12; :: thesis: verum

end;

( ex u being Element of V st u in NonZero V implies V is non trivial RealLinearSpace )

proof

given u being Element of V such that A3: u in NonZero V ; :: thesis: V is non trivial RealLinearSpace
u <> 0. V by A3, ZFMISC_1:64;
hence V is non trivial RealLinearSpace by STRUCT_0:def 19; :: thesis: verum

end;

hence ( V is non trivial RealLinearSpace iff ex u being Element of V st u in NonZero V ) by A1; :: thesis: verum