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

proof

assume V is non trivial RealLinearSpace ; :: thesis: ex u being Element of V st u in Proper_Vectors_of V
then consider u being Element of V such that
A2: u <> 0. V by Def8;
reconsider u = u as Element of V ;
A3: ( u in Proper_Vectors_of V iff not u is zero ) by Th26;
take u ; :: thesis: u in Proper_Vectors_of V
thus u in Proper_Vectors_of V by A2, A3, STRUCT_0:def 15; :: thesis: verum

end;

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

proof

given u being Element of V such that A4: u in Proper_Vectors_of V ; :: thesis: V is non trivial RealLinearSpace
u <> 0. V by A4, Def4;
hence V is non trivial RealLinearSpace by Def8; :: thesis: verum

end;

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