let t be 1 _greater Nat; :: thesis: (Partial_Union (Equal_Div_interval t)) . (t - 1) = [.0,1.[
A0: 0 <= t - 1 by Lm1, XREAL_1:50;
(Partial_Union (Equal_Div_interval t)) . (t - 1) = [.0,(((t - 1) + 1) / t).[ by A0, Lm3
.= [.0,1.[ by Lm1 ;
hence (Partial_Union (Equal_Div_interval t)) . (t - 1) = [.0,1.[ ; :: thesis: verum