thus
the_set_of_all_closed_real_bounded_intervals is cap-closed
( the_set_of_all_closed_real_bounded_intervals is with_empty_element & the_set_of_all_closed_real_bounded_intervals is with_countable_Cover )proof
now for x, y being set st x in the_set_of_all_closed_real_bounded_intervals & y in the_set_of_all_closed_real_bounded_intervals holds
x /\ y in the_set_of_all_closed_real_bounded_intervals let x,
y be
set ;
( x in the_set_of_all_closed_real_bounded_intervals & y in the_set_of_all_closed_real_bounded_intervals implies x /\ y in the_set_of_all_closed_real_bounded_intervals )assume that A1:
x in the_set_of_all_closed_real_bounded_intervals
and A2:
y in the_set_of_all_closed_real_bounded_intervals
;
x /\ y in the_set_of_all_closed_real_bounded_intervals consider a1,
b1 being
Real such that A3:
x = [.a1,b1.]
by A1;
consider a2,
b2 being
Real such that A4:
y = [.a2,b2.]
by A2;
[.a1,b1.] /\ [.a2,b2.] = [.(max (a1,a2)),(min (b1,b2)).]
by XXREAL_1:140;
hence
x /\ y in the_set_of_all_closed_real_bounded_intervals
by A3, A4;
verum end;
hence
the_set_of_all_closed_real_bounded_intervals is
cap-closed
by FINSUB_1:def 2;
verum
end;
[.1,0.] = {}
by XXREAL_1:29;
then
{} in the_set_of_all_closed_real_bounded_intervals
;
hence
the_set_of_all_closed_real_bounded_intervals is with_empty_element
; the_set_of_all_closed_real_bounded_intervals is with_countable_Cover
ex XX being countable Subset of the_set_of_all_closed_real_bounded_intervals st XX is Cover of REAL
hence
the_set_of_all_closed_real_bounded_intervals is with_countable_Cover
by SRINGS_1:def 4; verum