let v be FinSequence of REAL ; :: thesis: ( v <> {} implies Incr v <> {} )
assume A1: v <> {} ; :: thesis: Incr v <> {}
A2: len (Incr v) = card (rng v) by Def2;
assume Incr v = {} ; :: thesis: contradiction
then rng v = {} by A2;
hence contradiction by A1, RELAT_1:64; :: thesis: verum