set D = rng (W .flowSeq EL);

now :: thesis: ( W is trivial implies ex IT being Nat st
( IT in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
IT <= k ) ) )

assume W is trivial ; :: thesis: ex IT being Nat st
( IT in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
IT <= k ) )
then W .edges() <> {} by GLIB_001:136;
then rng (W .edgeSeq()) <> {} by GLIB_001:def 17;
then consider y being object such that
A2: y in rng (W .edgeSeq()) by XBOOLE_0:def 1;
consider x being object such that
A3: x in dom (W .edgeSeq()) and
y = (W .edgeSeq()) . x by A2, FUNCT_1:def 3;
x in dom (W .flowSeq EL) by A1, A3, Def15;
then (W .flowSeq EL) . x in rng (W .flowSeq EL) by FUNCT_1:def 3;
then reconsider D = rng (W .flowSeq EL) as non empty finite Subset of NAT ;
deffunc H₁( Nat) -> Nat = $1;
consider IT being Element of D such that
A4: for k being Element of D holds H₁(IT) <= H₁(k) from PRE_CIRC:sch 5();
reconsider IT = IT as Nat ;
take IT = IT; :: thesis: ( IT in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
IT <= k ) )
thus IT in rng (W .flowSeq EL) ; :: thesis: for k being Real st k in rng (W .flowSeq EL) holds
IT <= k
let k be Real; :: thesis: ( k in rng (W .flowSeq EL) implies IT <= k )
assume k in rng (W .flowSeq EL) ; :: thesis: IT <= k
hence IT <= k by A4; :: thesis: verum

end;

hence ( ( W is trivial implies ex b₁ being Nat st
( b₁ in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
b₁ <= k ) ) ) & ( W is trivial implies ex b₁ being Nat st b₁ = 0 ) ) ; :: thesis: verum