let V be RealNormSpace; :: thesis: ( not V is trivial implies not DualSp V is trivial )
assume not V is trivial ; :: thesis: not DualSp V is trivial
then consider F being Point of (DualSp V) such that
A1: ||.F.|| = 1 by Lm65A;
F <> 0. (DualSp V) by A1;
hence not DualSp V is trivial ; :: thesis: verum