let S be Subset-Family of REAL; :: thesis:
assume A1: S = { s where s is Subset of REAL : s is left_open_interval } ; :: thesis:
A2: S is cap-closed

proof

for S1, S2 being set st S1 in S & S2 in S holds
S1 /\ S2 in S

proof

let S1, S2 be set ; :: thesis:
assume A3: S1 in S ; :: thesis:
assume A4: S2 in S ; :: thesis:
consider s1 being Subset of REAL such that
A5: ( S1 = s1 & s1 is left_open_interval ) by A1, A3;
consider s2 being Subset of REAL such that
A6: ( S2 = s2 & s2 is left_open_interval ) by A1, A4;
set S3 = s1 /\ s2;
reconsider S3 = s1 /\ s2 as Subset of REAL ;
consider a1 being R_eal, b1 being Real such that
A7: s1 = ].a1,b1.] by MEASURE5:def 5, A5;
consider a2 being R_eal, b2 being Real such that
A8: s2 = ].a2,b2.] by MEASURE5:def 5, A6;
A9: S3 = ].(max (a1,a2)),(min (b1,b2)).] by A7, A8, XXREAL_1:141;
set m1 = max (a1,a2);
max (a1,a2) in ExtREAL by XXREAL_0:def 1;
then S3 is left_open_interval by A9, MEASURE5:def 5;
hence S1 /\ S2 in S by A1, A5, A6; :: thesis:

end;

hence S is cap-closed by FINSUB_1:def 2; :: thesis:

end;

A10: S is with_empty_element

proof

].0,0.] is left_open_interval

proof

0 in REAL by NUMBERS:19;
hence ].0,0.] is left_open_interval by NUMBERS:31, MEASURE5:def 5; :: thesis:

end;

then {} in S by A1;
hence S is with_empty_element ; :: thesis:

end;

then A12: not S is empty ;
S is diff-finite-partition-closed

proof

for S3, S4 being Element of S st not S3 \ S4 is empty holds
ex z being finite Subset of S st z is a_partition of S3 \ S4

proof

let S3, S4 be Element of S; :: thesis:
assume A13: not S3 \ S4 is empty ; :: thesis:
A14: ( S3 in S & S4 in S ) by A12;
consider s3 being Subset of REAL such that
A15: ( S3 = s3 & s3 is left_open_interval ) by A1, A14;
consider s4 being Subset of REAL such that
A16: ( S4 = s4 & s4 is left_open_interval ) by A1, A14;
consider a1 being R_eal, b1 being Real such that
A17: s3 = ].a1,b1.] by A15, MEASURE5:def 5;
consider a2 being R_eal, b2 being Real such that
A18: s4 = ].a2,b2.] by A16, MEASURE5:def 5;
A20: ( s4 is empty implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume A21: s4 is empty ; :: thesis:
set z = {S3};
A22: {S3} c= S by A14, TARSKI:def 1;
{S3} is a_partition of S3 by A13, EQREL_1:39;
hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A22, A16, A21; :: thesis:

end;

A23: ( not s4 is empty & s3 misses s4 implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume A24: ( not s4 is empty & s3 misses s4 ) ; :: thesis:
A25: S3 \ S4 = S3

proof

S3 c= S3 \ S4

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A27: x in S3 ; :: thesis:
not x in S4 by A27, A15, A16, A24, XBOOLE_0:def 4;
hence x in S3 \ S4 by A27, XBOOLE_0:def 5; :: thesis:

end;

hence S3 \ S4 = S3 ; :: thesis:

end;

set z = {S3};
A28: {S3} c= S by A14, TARSKI:def 1;
{S3} is a_partition of S3 by A13, EQREL_1:39;
hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A28, A25; :: thesis:

end;

( not s4 is empty & s3 meets s4 implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume A29: ( not s4 is empty & s3 meets s4 ) ; :: thesis:
then A30: ].a1,b1.] \ ].a2,b2.] = ].a1,a2.] \/ ].b2,b1.] by A17, A18, XXREAL_1:199;
A31: ( b1 <= b2 implies ].a1,a2.] /\ ].b2,b1.] c= {} )

proof

assume A32: b1 <= b2 ; :: thesis:
].b2,b1.] = {}

proof

assume ].b2,b1.] <> {} ; :: thesis:
then consider x being object such that
A33: x in ].b2,b1.] by XBOOLE_0:def 1;
reconsider x = x as real number by A33;
( b2 < x & x <= b1 ) by A33, XXREAL_1:2;
hence contradiction by A32, XXREAL_0:2; :: thesis:

end;

hence ].a1,a2.] /\ ].b2,b1.] c= {} ; :: thesis:

end;

A33a: ( b2 < b1 implies ].a1,a2.] /\ ].b2,b1.] c= {} )

proof

assume b2 < b1 ; :: thesis:
].a1,a2.] /\ ].b2,b1.] c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A34: x in ].a1,a2.] /\ ].b2,b1.] ; :: thesis:
then A35: ( x in ].a1,a2.] & x in ].b2,b1.] ) by XBOOLE_0:def 4;
reconsider x = x as real number by A34;

per cases ;

suppose A36: a2 <= b2 ; :: thesis:

( b2 < x & x <= a2 ) by A35, XXREAL_1:2;
hence x in {} by A36, XXREAL_0:2; :: thesis:

end;

suppose A37: b2 < a2 ; :: thesis:

s4 c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A38: x in s4 ; :: thesis:
then reconsider x = x as real number ;
( a2 < x & x <= b2 ) by A18, A38, XXREAL_1:2;
hence x in {} by A37, XXREAL_0:2; :: thesis:

end;

hence x in {} by A29; :: thesis:

end;

end;

end;

hence ].a1,a2.] /\ ].b2,b1.] c= {} ; :: thesis:

end;

A40: ( a2 in REAL or a2 in {-infty,+infty} ) by XBOOLE_0:def 3;
A41: ( a2 = +infty implies ex z being finite Subset of S st z is a_partition of S3 \ S4 ) by A18, A29, XXREAL_1:216;
A42: ( a2 = -infty implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume A43: a2 = -infty ; :: thesis:
A44: S3 \ S4 = {} \/ ].b2,b1.] by A15, A16, A17, A18, A30, A43, XXREAL_1:212;
set z = {].b2,b1.]};
A45: {].b2,b1.]} c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A47: x in {].b2,b1.]} ; :: thesis:
then A48: x = ].b2,b1.] by TARSKI:def 1;
reconsider x = x as Subset of REAL by A47, TARSKI:def 1;
b2 in REAL by XREAL_0:def 1;
then x is left_open_interval by A48, NUMBERS:31, MEASURE5:def 5;
hence x in S by A1; :: thesis:

end;

{].b2,b1.]} is a_partition of S3 \ S4 by A44, A13, EQREL_1:39;
hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A45; :: thesis:

end;

A49: ( a2 in REAL & ( a1 < a2 or b2 < b1 ) & ( not a1 < a2 or not b2 < b1 ) implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume A50: a2 in REAL ; :: thesis:
assume A51: ( ( a1 < a2 or b2 < b1 ) & ( not a1 < a2 or not b2 < b1 ) ) ; :: thesis:
A52: ( a1 < a2 & b1 <= b2 implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume A53: ( a1 < a2 & b1 <= b2 ) ; :: thesis:
].b2,b1.] c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A54: x in ].b2,b1.] ; :: thesis:
then reconsider x = x as real number ;
( b2 < x & x <= b1 ) by A54, XXREAL_1:2;
hence x in {} by A53, XXREAL_0:2; :: thesis:

end;

then A55: ].b2,b1.] = {} ;
set z = {].a1,a2.]};
A56: {].a1,a2.]} c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A57: x in {].a1,a2.]} ; :: thesis:
].a1,a2.] in S

proof

set AA = ].a1,a2.];
reconsider AA = ].a1,a2.] as Subset of REAL by A50, XXREAL_1:227;
AA is left_open_interval by A50, MEASURE5:def 5;
hence ].a1,a2.] in S by A1; :: thesis:

end;

hence x in S by A57, TARSKI:def 1; :: thesis:

end;

].a1,a2.] <> {}

proof

a2 in ].a1,a2.] by A53;
hence ].a1,a2.] <> {} ; :: thesis:

end;

then {].a1,a2.]} is a_partition of ].a1,a2.] by EQREL_1:39;
hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A15, A16, A17, A18, A30, A55, A56; :: thesis:

end;

( b2 < b1 & a2 <= a1 implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume A58: ( b2 < b1 & a2 <= a1 ) ; :: thesis:
].a1,a2.] c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A59: x in ].a1,a2.] ; :: thesis:
then reconsider x = x as real number by A50;
( a1 < x & x <= a2 ) by A59, XXREAL_1:2;
hence x in {} by A58, XXREAL_0:2; :: thesis:

end;

then A60: ].a1,a2.] = {} ;
set z = {].b2,b1.]};
A61: {].b2,b1.]} c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A62: x in {].b2,b1.]} ; :: thesis:
].b2,b1.] in S

proof

set AA = ].b2,b1.];
reconsider AA = ].b2,b1.] as Subset of REAL ;
b2 in REAL by XREAL_0:def 1;
then AA is left_open_interval by NUMBERS:31, MEASURE5:def 5;
hence ].b2,b1.] in S by A1; :: thesis:

end;

hence x in S by A62, TARSKI:def 1; :: thesis:

end;

].b2,b1.] <> {} by A58, XXREAL_1:2;
then {].b2,b1.]} is a_partition of ].b2,b1.] by EQREL_1:39;
hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A15, A16, A17, A18, A30, A60, A61; :: thesis:

end;

hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A51, A52; :: thesis:

end;

A63: ( a2 in REAL & not a1 < a2 & not b2 < b1 implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume a2 in REAL ; :: thesis:
assume A64: ( not a1 < a2 & not b2 < b1 ) ; :: thesis:
S3 \ S4 c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A65: x in S3 \ S4 ; :: thesis:
then A66: ( x in ].a1,b1.] & not x in ].a2,b2.] ) by A15, A16, A17, A18, XBOOLE_0:def 5;
reconsider x = x as real number by A15, A65;
( a1 < x & x <= b1 & ( x <= a2 or b2 < x ) ) by A66, XXREAL_1:2;
hence x in {} by A64, XXREAL_0:2; :: thesis:

end;

hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A13; :: thesis:

end;

( a2 in REAL & a1 < a2 & b2 < b1 implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume A67: a2 in REAL ; :: thesis:
assume ( a1 < a2 & b2 < b1 ) ; :: thesis:
then A69: ( ].a1,a2.] <> {} & ].b2,b1.] <> {} ) by XXREAL_1:2;
set z = {].a1,a2.],].b2,b1.]};
A70: {].a1,a2.],].b2,b1.]} c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A71: x in {].a1,a2.],].b2,b1.]} ; :: thesis:
A72: ].a1,a2.] in S

proof

set AA = ].a1,a2.];
reconsider AA = ].a1,a2.] as Subset of REAL by A67, XXREAL_1:227;
AA is left_open_interval by A67, MEASURE5:def 5;
hence ].a1,a2.] in S by A1; :: thesis:

end;

].b2,b1.] in S

proof

set BB = ].b2,b1.];
reconsider BB = ].b2,b1.] as Subset of REAL ;
b2 in REAL by XREAL_0:def 1;
then BB is left_open_interval by NUMBERS:31, MEASURE5:def 5;
hence ].b2,b1.] in S by A1; :: thesis:

end;

hence x in S by A71, A72, TARSKI:def 2; :: thesis:

end;

{].a1,a2.],].b2,b1.]} is a_partition of ].a1,b1.] \ ].a2,b2.]

proof

A73: {].a1,a2.],].b2,b1.]} is Subset-Family of (].a1,b1.] \ ].a2,b2.])

proof

{].a1,a2.],].b2,b1.]} c= bool (].a1,b1.] \ ].a2,b2.])

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {].a1,a2.],].b2,b1.]} ; :: thesis:
then A74: ( x = ].a1,a2.] or x = ].b2,b1.] ) by TARSKI:def 2;
reconsider x = x as set by TARSKI:1;
x c= ].a1,b1.] \ ].a2,b2.]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in x ; :: thesis:
then y in ].a1,a2.] \/ ].b2,b1.] by A74, XBOOLE_0:def 3;
hence y in ].a1,b1.] \ ].a2,b2.] by A17, A18, A29, XXREAL_1:199; :: thesis:

end;

hence x in bool (].a1,b1.] \ ].a2,b2.]) ; :: thesis:

end;

hence {].a1,a2.],].b2,b1.]} is Subset-Family of (].a1,b1.] \ ].a2,b2.]) ; :: thesis:

end;

A75: union {].a1,a2.],].b2,b1.]} = ].a1,b1.] \ ].a2,b2.] by A30, ZFMISC_1:75;
for A being Subset of (].a1,b1.] \ ].a2,b2.]) st A in {].a1,a2.],].b2,b1.]} holds
( A <> {} & ( for B being Subset of (].a1,b1.] \ ].a2,b2.]) holds
( not B in {].a1,a2.],].b2,b1.]} or A = B or A misses B ) ) )

proof

let A be Subset of (].a1,b1.] \ ].a2,b2.]); :: thesis:
assume A76: A in {].a1,a2.],].b2,b1.]} ; :: thesis:
for B being Subset of (].a1,b1.] \ ].a2,b2.]) holds
( not B in {].a1,a2.],].b2,b1.]} or A = B or A misses B )

proof

let B be Subset of (].a1,b1.] \ ].a2,b2.]); :: thesis:
assume B in {].a1,a2.],].b2,b1.]} ; :: thesis:
then ( ( A = ].a1,a2.] & B = ].a1,a2.] ) or ( A = ].a1,a2.] & B = ].b2,b1.] ) or ( A = ].b2,b1.] & B = ].a1,a2.] ) or ( A = ].b2,b1.] & B = ].b2,b1.] ) ) by A76, TARSKI:def 2;
hence ( A = B or A misses B ) by A31, A33a; :: thesis:

end;

hence ( A <> {} & ( for B being Subset of (].a1,b1.] \ ].a2,b2.]) holds
( not B in {].a1,a2.],].b2,b1.]} or A = B or A misses B ) ) ) by A69, A76; :: thesis:

end;

hence {].a1,a2.],].b2,b1.]} is a_partition of ].a1,b1.] \ ].a2,b2.] by A73, A75, EQREL_1:def 4; :: thesis:

end;

hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A15, A16, A17, A18, A70; :: thesis:

end;

hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A40, A41, A42, A49, A63, TARSKI:def 2; :: thesis:

end;

hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A20, A23; :: thesis:

end;

hence S is diff-finite-partition-closed by SRINGS_1:def 2; :: thesis:

end;

hence ( S is cap-closed & S is diff-finite-partition-closed & S is with_empty_element & S is with_countable_Cover ) by A1, A2, A10, LemmB; :: thesis: