let IT1, IT2 be Nat; :: thesis: ( ( W is trivial & IT1 in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
IT1 <= k ) & IT2 in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
IT2 <= k ) implies IT1 = IT2 ) & ( W is trivial & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) )

hereby :: thesis: ( W is trivial & IT1 = 0 & IT2 = 0 implies IT1 = IT2 )

assume W is trivial ; :: thesis: ( IT1 in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
IT1 <= k ) & IT2 in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
IT2 <= k ) implies IT1 = IT2 )
assume that
A5: IT1 in rng (W .flowSeq EL) and
A6: for k being Real st k in rng (W .flowSeq EL) holds
IT1 <= k ; :: thesis: ( IT2 in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
IT2 <= k ) implies IT1 = IT2 )
assume that
A7: IT2 in rng (W .flowSeq EL) and
A8: for k being Real st k in rng (W .flowSeq EL) holds
IT2 <= k ; :: thesis: IT1 = IT2
A9: IT2 <= IT1 by A5, A8;
IT1 <= IT2 by A6, A7;
hence IT1 = IT2 by A9, XXREAL_0:1; :: thesis: verum

end;

thus ( W is trivial & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) ; :: thesis: verum