let V be RealLinearSpace; :: thesis: for u being Element of V holds
( u in Proper_Vectors_of V iff not u is zero )
let u be Element of V; :: thesis: ( u in Proper_Vectors_of V iff not u is zero )
thus ( u in Proper_Vectors_of V implies not u is zero ) :: thesis: ( not u is zero implies u in Proper_Vectors_of V )

proof

assume u in Proper_Vectors_of V ; :: thesis: not u is zero
then u <> 0. V by Def4;
hence not u is zero by STRUCT_0:def 15; :: thesis: verum

end;

thus ( not u is zero implies u in Proper_Vectors_of V ) :: thesis: verum

proof

assume not u is zero ; :: thesis: u in Proper_Vectors_of V
then u <> 0. V by STRUCT_0:def 15;
hence u in Proper_Vectors_of V by Def4; :: thesis: verum

end;