let t be 1 _greater Nat; :: thesis: for r being Real st r in [.0,1.[ holds
ex i being Nat st
( i <= t - 1 & r in (Equal_Div_interval t) . i )
let r be Real; :: thesis: ( r in [.0,1.[ implies ex i being Nat st
( i <= t - 1 & r in (Equal_Div_interval t) . i ) )
assume r in [.0,1.[ ; :: thesis: ex i being Nat st
( i <= t - 1 & r in (Equal_Div_interval t) . i )
then A2: r in (Partial_Union (Equal_Div_interval t)) . (t - 1) by Lm6;
A3: t - 1 > 0 by Lm1, XREAL_1:50;
t - 1 in NAT by A3, INT_1:3;
hence ex i being Nat st
( i <= t - 1 & r in (Equal_Div_interval t) . i ) by A2, PROB_3:13; :: thesis: verum