reconsider S = (Seg n) --> the_set_of_all_right_open_real_bounded_intervals as n -element FinSequence by Th6;
for i being Nat st i in Seg n holds
S . i is with_empty_element cap-closed semi-diff-closed Subset-Family of ((ProductREAL n) . i)
proof
let i be Nat; :: thesis: ( i in Seg n implies S . i is with_empty_element cap-closed semi-diff-closed Subset-Family of ((ProductREAL n) . i) )
assume A1: i in Seg n ; :: thesis: S . i is with_empty_element cap-closed semi-diff-closed Subset-Family of ((ProductREAL n) . i)
then A2: ( S . i = the_set_of_all_right_open_real_bounded_intervals & (ProductREAL n) . i = REAL ) by FUNCOP_1:7;
reconsider Si = S . i as Subset-Family of REAL by A1, FUNCOP_1:7;
thus S . i is with_empty_element cap-closed semi-diff-closed Subset-Family of ((ProductREAL n) . i) by A2, SRINGS_3:10; :: thesis: verum
end;
hence (Seg n) --> the_set_of_all_right_open_real_bounded_intervals is ClassicalSemiringFamily of ProductREAL n by SRINGS_4:def 6; :: thesis: verum