let V be RealNormSpace; :: thesis: ( not V is trivial implies ex F being Point of (DualSp V) st ||.F.|| = 1 )
assume not V is trivial ; :: thesis: ex F being Point of (DualSp V) st ||.F.|| = 1
then consider x0 being Element of V such that
P1: x0 <> 0. V ;
ex F being Point of (DualSp V) st
( ||.F.|| = 1 & (Bound2Lipschitz (F,V)) . x0 = ||.x0.|| ) by Lm65, P1;
hence ex F being Point of (DualSp V) st ||.F.|| = 1 ; :: thesis: verum