let p be FinSequence; :: thesis: ( p <> {} iff len p >= 1 )
hereby :: thesis: ( len p >= 1 implies p <> {} )
assume p <> {} ; :: thesis: len p >= 1
then (len p) + 1 > 0 + 1 by XREAL_1:8;
hence len p >= 1 by NAT_1:13; :: thesis: verum
end;
assume len p >= 1 ; :: thesis: p <> {}
hence p <> {} ; :: thesis: verum