assume W is V5() ; :: 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