{ I where I is Subset of REAL : I is right_open_interval } c= bool REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { I where I is Subset of REAL : I is right_open_interval } or x in bool REAL )
assume x in { I where I is Subset of REAL : I is right_open_interval } ; :: thesis: x in bool REAL
then consider I being Subset of REAL such that
A1: x = I and
I is right_open_interval ;
thus x in bool REAL by A1; :: thesis: verum

end;

then reconsider S = { I where I is Subset of REAL : I is right_open_interval } as Subset-Family of REAL ;
A2: S is cap-closed by SRINGS_3:27;

now :: thesis: for A, B being set st A in the_set_of_all_right_open_real_bounded_intervals & B in the_set_of_all_right_open_real_bounded_intervals holds
A /\ B in the_set_of_all_right_open_real_bounded_intervals

let A, B be set ; :: thesis: ( A in the_set_of_all_right_open_real_bounded_intervals & B in the_set_of_all_right_open_real_bounded_intervals implies b₁ /\ b₂ in the_set_of_all_right_open_real_bounded_intervals )
assume A3: ( A in the_set_of_all_right_open_real_bounded_intervals & B in the_set_of_all_right_open_real_bounded_intervals ) ; :: thesis: b₁ /\ b₂ in the_set_of_all_right_open_real_bounded_intervals
then A4: ( A in S & B in S ) by Th27;
then consider I being Subset of REAL such that
A5: ( A = I & I is right_open_interval ) ;
consider J being Subset of REAL such that
A6: ( B = J & J is right_open_interval ) by A4;
( S is cap-closed & I in S & J in S ) by A5, A6, SRINGS_3:27;
then I /\ J in S by FINSUB_1:def 2;
then consider K being Subset of REAL such that
A7: I /\ J = K and
A8: K is right_open_interval ;
consider a being Real, b being R_eal such that
A9: K = [.a,b.[ by A8, MEASURE5:def 4;

per cases ( not K is empty or K is empty ) ;

suppose A10: not K is empty ; :: thesis: b₁ /\ b₂ in the_set_of_all_right_open_real_bounded_intervals

consider x being object such that
A11: x in K by A10;
reconsider x = x as Real by A11;
b is Real

proof

assume b is not Real ; :: thesis: contradiction
then ( not b in REAL & a in REAL & a <= b ) by XREAL_0:def 1, A10, A9, XXREAL_1:27;
then A12: b = +infty by XXREAL_0:10;
a <= x by A11, A9, XXREAL_1:3;
then A13: ( [.x,+infty.[ c= A & [.x,+infty.[ c= B ) by A9, A12, XXREAL_1:38, A5, A6, A7, XBOOLE_1:18;
consider xa, xb being Real such that
A14: A = [.xa,xb.[ by A3;
A15: not xb in A by A14, XXREAL_1:3;

per cases ( xb < x or x <= xb ) ;

suppose xb < x ; :: thesis: contradiction

then A16: not x in A by A14, XXREAL_1:3;
x < b by A11, A9, XXREAL_1:3;
hence contradiction by A16, A13, A12, XXREAL_1:3; :: thesis: verum

end;

suppose x <= xb ; :: thesis: contradiction

hence contradiction by A15, A13, XXREAL_1:236; :: thesis: verum

end;

end;

end;

then reconsider b = b as Real ;
K = [.a,b.[ by A9;
hence A /\ B in the_set_of_all_right_open_real_bounded_intervals by A7, A5, A6; :: thesis: verum

end;

suppose K is empty ; :: thesis: b₁ /\ b₂ in the_set_of_all_right_open_real_bounded_intervals

hence A /\ B in the_set_of_all_right_open_real_bounded_intervals by A7, A5, A6, Th28, SETFAM_1:def 8; :: thesis: verum

end;

end;

end;

hence the_set_of_all_right_open_real_bounded_intervals is cap-closed by FINSUB_1:def 2; :: thesis: ( the_set_of_all_right_open_real_bounded_intervals is diff-finite-partition-closed & the_set_of_all_right_open_real_bounded_intervals is with_empty_element )

now :: thesis: for A, B being Element of the_set_of_all_right_open_real_bounded_intervals st not A \ B is empty holds
ex x being finite Subset of the_set_of_all_right_open_real_bounded_intervals st x is a_partition of A \ B

let A, B be Element of the_set_of_all_right_open_real_bounded_intervals ; :: thesis: ( not A \ B is empty implies ex x being finite Subset of the_set_of_all_right_open_real_bounded_intervals st x is a_partition of A \ B )
assume A17: not A \ B is empty ; :: thesis: ex x being finite Subset of the_set_of_all_right_open_real_bounded_intervals st x is a_partition of A \ B
A18: ( A in S & B in S ) by Th27;
then consider I being Subset of REAL such that
A19: A = I and
I is right_open_interval ;
consider J being Subset of REAL such that
A20: B = J and
J is right_open_interval by A18;
( S is semi-diff-closed & not S is empty ) by SRINGS_3:27;
then S is diff-c=-finite-partition-closed by SRINGS_3:9;
then ( S is diff-finite-partition-closed & I is Element of S & J is Element of S & not I \ J is empty ) by A17, A19, A20, A2, Th27;
then consider x being finite Subset of S such that
A21: x is a_partition of I \ J by SRINGS_1:def 2;

now :: thesis: ( x is finite Subset of the_set_of_all_right_open_real_bounded_intervals & x is a_partition of A \ B )

x in bool the_set_of_all_right_open_real_bounded_intervals

proof

reconsider x1 = x as set ;
x1 c= the_set_of_all_right_open_real_bounded_intervals

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in x1 or t in the_set_of_all_right_open_real_bounded_intervals )
assume A22: t in x1 ; :: thesis: t in the_set_of_all_right_open_real_bounded_intervals
then t in S ;
then consider K being Subset of REAL such that
A23: t = K and
A24: K is right_open_interval ;

per cases ( K is empty or not K is empty ) ;

suppose K is empty ; :: thesis: t in the_set_of_all_right_open_real_bounded_intervals

hence t in the_set_of_all_right_open_real_bounded_intervals by A23, Th28, SETFAM_1:def 8; :: thesis: verum

end;

suppose A25: not K is empty ; :: thesis: t in the_set_of_all_right_open_real_bounded_intervals

consider a being Real, b being R_eal such that
A26: K = [.a,b.[ by A24, MEASURE5:def 4;
A27: ( K c= A \ B & A \ B c= A ) by A22, A23, A21, A19, A20, XBOOLE_1:36;
A in the_set_of_all_right_open_real_bounded_intervals ;
then consider e, c being Real such that
A28: A = [.e,c.[ ;

now :: thesis: ( a is Real & c is Real & b is R_eal & a < b & [.a,b.[ c= [.a,c.[ )

thus ( a is Real & c is Real ) ; :: thesis: ( b is R_eal & a < b & [.a,b.[ c= [.a,c.[ )
thus b is R_eal ; :: thesis: ( a < b & [.a,b.[ c= [.a,c.[ )
thus a < b by A25, A26, XXREAL_1:27; :: thesis: [.a,b.[ c= [.a,c.[

now :: thesis: for x being object st x in [.a,b.[ holds
x in [.a,c.[

let x be object ; :: thesis: ( x in [.a,b.[ implies x in [.a,c.[ )
assume A29: x in [.a,b.[ ; :: thesis: x in [.a,c.[
then A30: x in [.e,c.[ by A26, A27, A28;
reconsider x1 = x as ExtReal by A29;
( a <= x1 & x1 < b & e <= x1 & x1 < c ) by A29, A30, XXREAL_1:3;
hence x in [.a,c.[ by XXREAL_1:3; :: thesis: verum

end;

hence [.a,b.[ c= [.a,c.[ ; :: thesis: verum

end;

then b is Real by Th4;
hence t in the_set_of_all_right_open_real_bounded_intervals by A26, A23; :: thesis: verum

end;

end;

end;

hence x in bool the_set_of_all_right_open_real_bounded_intervals ; :: thesis: verum

end;

hence x is finite Subset of the_set_of_all_right_open_real_bounded_intervals ; :: thesis: x is a_partition of A \ B
reconsider x1 = x as Subset-Family of (A \ B) by A21, A19, A20;
thus x is a_partition of A \ B by A19, A20, A21; :: thesis: verum

end;

hence ex x being finite Subset of the_set_of_all_right_open_real_bounded_intervals st x is a_partition of A \ B ; :: thesis: verum

end;

hence ( the_set_of_all_right_open_real_bounded_intervals is diff-finite-partition-closed & the_set_of_all_right_open_real_bounded_intervals is with_empty_element ) by SRINGS_1:def 2, Th28; :: thesis: verum