( W is trivial iff W .length() = 0 )

proof

hereby :: thesis: ( W .length() = 0 implies W is trivial )

assume A1: W is trivial ; :: thesis: W .length() = 0
W <> {}

proof

assume W = {} ; :: thesis: contradiction
then len W = 0 ;
hence contradiction ; :: thesis: verum

end;

then consider x being object such that
A5: W = <*x*> by A1, JORDAN1G:1;
set WW = W .edgeSeq() ;
len W = 1 by A5, FINSEQ_1:39;
then (2 * (len (W .edgeSeq()))) + 1 = 0 + 1 by Def15;
hence W .length() = 0 ; :: thesis: verum

end;

assume W .length() = 0 ; :: thesis: W is trivial
then len W = (2 * 0) + 1 by Def15;
hence W is trivial by NAT_D:60; :: thesis: verum

end;

hence ( W is trivial iff W .length() = 0 ) ; :: thesis: verum