let S be Subset-Family of REAL; :: thesis: ( S = {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } implies ( S is cap-closed & S is diff-finite-partition-closed with_empty_element Subset-Family of REAL ) )
assume A1: S = {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ; :: thesis: ( S is cap-closed & S is diff-finite-partition-closed with_empty_element Subset-Family of REAL )
A2: S is with_empty_element

proof

{} in {{}} by TARSKI:def 1;
then {} in S by A1, XBOOLE_0:def 3;
hence S is with_empty_element ; :: thesis: verum

end;

A3: S is cap-closed

proof

let e1, e2 be set ; :: according to FINSUB_1:def 2 :: thesis: ( not e1 in S or not e2 in S or e1 /\ e2 in S )
assume A4: e1 in S ; :: thesis: ( not e2 in S or e1 /\ e2 in S )
assume A5: e2 in S ; :: thesis: e1 /\ e2 in S
A6: ( e1 in {{}} or e1 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ) by A1, A4, XBOOLE_0:def 3;
A7: ( e2 in {{}} or e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ) by A1, A5, XBOOLE_0:def 3;
A8: ( e1 = {} implies e1 /\ e2 in S )

proof

assume e1 = {} ; :: thesis: e1 /\ e2 in S
then e1 /\ e2 in {{}} by TARSKI:def 1;
hence e1 /\ e2 in S by A1, XBOOLE_0:def 3; :: thesis: verum

end;

A9: ( e2 = {} implies e1 /\ e2 in S )

proof

assume e2 = {} ; :: thesis: e1 /\ e2 in S
then e1 /\ e2 in {{}} by TARSKI:def 1;
hence e1 /\ e2 in S by A1, XBOOLE_0:def 3; :: thesis: verum

end;

( e1 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } & e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } implies e1 /\ e2 in S )

proof

assume A10: e1 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ; :: thesis: ( not e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } or e1 /\ e2 in S )
assume A11: e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ; :: thesis: e1 /\ e2 in S
consider E1 being Subset of REAL such that
A12: ( e1 = E1 & ex a1, b1 being Real st
( a1 < b1 & ( for x being real number holds
( x in E1 iff ( a1 < x & x <= b1 ) ) ) ) ) by A10;
consider E2 being Subset of REAL such that
A13: ( e2 = E2 & ex a2, b2 being Real st
( a2 < b2 & ( for x being real number holds
( x in E2 iff ( a2 < x & x <= b2 ) ) ) ) ) by A11;
consider a1, b1 being Real such that
A14: ( a1 < b1 & ( for x being real number holds
( x in E1 iff ( a1 < x & x <= b1 ) ) ) ) by A12;
consider a2, b2 being Real such that
A15: ( a2 < b2 & ( for x being real number holds
( x in E2 iff ( a2 < x & x <= b2 ) ) ) ) by A13;
e1 /\ e2 in {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }

proof

A16: ( b1 <= a2 implies e1 /\ e2 in {{}} )

proof

assume A17: b1 <= a2 ; :: thesis: e1 /\ e2 in {{}}
e1 /\ e2 c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in e1 /\ e2 or x in {} )
assume A18: x in e1 /\ e2 ; :: thesis: x in {}
then A19: ( x in e1 & x in e2 ) by XBOOLE_0:def 4;
reconsider x = x as real number by A13, A18;
( a1 < x & x <= b1 & a2 < x & x <= b2 ) by A12, A13, A14, A15, A19;
hence x in {} by A17, XXREAL_0:2; :: thesis: verum

end;

then e1 /\ e2 = {} ;
hence e1 /\ e2 in {{}} by TARSKI:def 1; :: thesis: verum

end;

A20: ( a2 < b1 & a1 < b2 & not e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } implies e1 /\ e2 in {{}} )

proof

set P = { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ;
assume ( a2 < b1 & a1 < b2 ) ; :: thesis: ( e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } or e1 /\ e2 in {{}} )
A21: ( a2 < a1 & b2 < b1 & a1 < b2 implies e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } )

proof

assume A22: ( a2 < a1 & b2 < b1 ) ; :: thesis: ( not a1 < b2 or e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } )
assume A23: a1 < b2 ; :: thesis: e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }
A24: for x being real number holds
( x in e1 /\ e2 iff ( a1 < x & x <= b2 ) )

proof

A25: for x being real number st x in e1 /\ e2 holds
( a1 < x & x <= b2 )

proof

let x be real number ; :: thesis: ( x in e1 /\ e2 implies ( a1 < x & x <= b2 ) )
assume x in e1 /\ e2 ; :: thesis: ( a1 < x & x <= b2 )
then ( x in e1 & x in e2 ) by XBOOLE_0:def 4;
hence ( a1 < x & x <= b2 ) by A12, A13, A14, A15; :: thesis: verum

end;

for x being real number st a1 < x & x <= b2 holds
x in e1 /\ e2

proof

let x be real number ; :: thesis: ( a1 < x & x <= b2 implies x in e1 /\ e2 )
assume A26: ( a1 < x & x <= b2 ) ; :: thesis: x in e1 /\ e2
then A27: x <= b1 by A22, XXREAL_0:2;
( a1 < x & a2 < a1 implies a2 < x ) by XXREAL_0:2;
then ( x in e1 & x in e2 ) by A12, A13, A14, A15, A22, A26, A27;
hence x in e1 /\ e2 by XBOOLE_0:def 4; :: thesis: verum

end;

hence for x being real number holds
( x in e1 /\ e2 iff ( a1 < x & x <= b2 ) ) by A25; :: thesis: verum

end;

e1 /\ e2 = E1 /\ E2 by A12, A13;
hence e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A23, A24; :: thesis: verum

end;

A28: ( a2 < a1 & b2 < b1 & not a1 < b2 implies e1 /\ e2 in {{}} )

proof

assume A29: ( a2 < a1 & b2 < b1 & not a1 < b2 ) ; :: thesis: e1 /\ e2 in {{}}
e1 /\ e2 c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in e1 /\ e2 or x in {} )
assume A30: x in e1 /\ e2 ; :: thesis: x in {}
then A31: ( x in e1 & x in e2 ) by XBOOLE_0:def 4;
reconsider x = x as real number by A12, A30;
( a1 < x & x <= b1 & a2 < x & x <= b2 ) by A12, A13, A14, A15, A31;
hence x in {} by A29, XXREAL_0:2; :: thesis: verum

end;

then e1 /\ e2 = {} ;
hence e1 /\ e2 in {{}} by TARSKI:def 1; :: thesis: verum

end;

A32: ( a2 < a1 & b1 <= b2 implies e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } )

proof

assume A33: ( a2 < a1 & b1 <= b2 ) ; :: thesis: e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }
A34: for x being real number holds
( x in e1 /\ e2 iff ( a1 < x & x <= b1 ) )

proof

A35: for x being real number st x in e1 /\ e2 holds
( a1 < x & x <= b1 )

proof

let x be real number ; :: thesis: ( x in e1 /\ e2 implies ( a1 < x & x <= b1 ) )
assume x in e1 /\ e2 ; :: thesis: ( a1 < x & x <= b1 )
then ( x in e1 & x in e2 ) by XBOOLE_0:def 4;
hence ( a1 < x & x <= b1 ) by A12, A14; :: thesis: verum

end;

for x being real number st a1 < x & x <= b1 holds
x in e1 /\ e2

proof

let x be real number ; :: thesis: ( a1 < x & x <= b1 implies x in e1 /\ e2 )
assume ( a1 < x & x <= b1 ) ; :: thesis: x in e1 /\ e2
then ( a1 < x & x <= b1 & a2 < x & x <= b2 ) by A33, XXREAL_0:2;
then ( x in e1 & x in e2 ) by A12, A13, A14, A15;
hence x in e1 /\ e2 by XBOOLE_0:def 4; :: thesis: verum

end;

hence for x being real number holds
( x in e1 /\ e2 iff ( a1 < x & x <= b1 ) ) by A35; :: thesis: verum

end;

e1 /\ e2 = E1 /\ E2 by A12, A13;
hence e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A14, A34; :: thesis: verum

end;

A37: ( a1 <= a2 & b2 < b1 implies e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } )

proof

assume A38: ( a1 <= a2 & b2 < b1 ) ; :: thesis: e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }
A39: for x being real number holds
( x in e1 /\ e2 iff ( a2 < x & x <= b2 ) )

proof

A40: for x being real number st x in e1 /\ e2 holds
( a2 < x & x <= b2 )

proof

let x be real number ; :: thesis: ( x in e1 /\ e2 implies ( a2 < x & x <= b2 ) )
assume x in e1 /\ e2 ; :: thesis: ( a2 < x & x <= b2 )
then ( x in e1 & x in e2 ) by XBOOLE_0:def 4;
hence ( a2 < x & x <= b2 ) by A13, A15; :: thesis: verum

end;

for x being real number st a2 < x & x <= b2 holds
x in e1 /\ e2

proof

let x be real number ; :: thesis: ( a2 < x & x <= b2 implies x in e1 /\ e2 )
assume A41: ( a2 < x & x <= b2 ) ; :: thesis: x in e1 /\ e2
A42: ( a2 < x & a1 <= a2 implies a1 < x ) by XXREAL_0:2;
( x <= b2 & b2 < b1 implies x <= b1 ) by XXREAL_0:2;
then ( x in e1 & x in e2 ) by A12, A13, A14, A15, A38, A41, A42;
hence x in e1 /\ e2 by XBOOLE_0:def 4; :: thesis: verum

end;

hence for x being real number holds
( x in e1 /\ e2 iff ( a2 < x & x <= b2 ) ) by A40; :: thesis: verum

end;

e1 /\ e2 = E1 /\ E2 by A12, A13;
hence e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A15, A39; :: thesis: verum

end;

A43: ( a1 <= a2 & b1 <= b2 & not a2 < b1 implies e1 /\ e2 in {{}} )

proof

assume A44: ( a1 <= a2 & b1 <= b2 & not a2 < b1 ) ; :: thesis: e1 /\ e2 in {{}}
e1 /\ e2 c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in e1 /\ e2 or x in {} )
assume A45: x in e1 /\ e2 ; :: thesis: x in {}
then A46: ( x in e1 & x in e2 ) by XBOOLE_0:def 4;
reconsider x = x as real number by A12, A45;
( a2 < x & x <= b1 ) by A12, A13, A14, A15, A46;
hence x in {} by A44, XXREAL_0:2; :: thesis: verum

end;

then e1 /\ e2 = {} ;
hence e1 /\ e2 in {{}} by TARSKI:def 1; :: thesis: verum

end;

( a1 <= a2 & b1 <= b2 & a2 < b1 implies e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } )

proof

assume A47: ( a1 <= a2 & b1 <= b2 & a2 < b1 ) ; :: thesis: e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }
A48: for x being real number holds
( x in e1 /\ e2 iff ( a2 < x & x <= b1 ) )

proof

A49: for x being real number st x in e1 /\ e2 holds
( a2 < x & x <= b1 )

proof

let x be real number ; :: thesis: ( x in e1 /\ e2 implies ( a2 < x & x <= b1 ) )
assume x in e1 /\ e2 ; :: thesis: ( a2 < x & x <= b1 )
then ( x in e1 & x in e2 ) by XBOOLE_0:def 4;
hence ( a2 < x & x <= b1 ) by A12, A13, A14, A15; :: thesis: verum

end;

for x being real number st a2 < x & x <= b1 holds
x in e1 /\ e2

proof

let x be real number ; :: thesis: ( a2 < x & x <= b1 implies x in e1 /\ e2 )
assume A50: ( a2 < x & x <= b1 ) ; :: thesis: x in e1 /\ e2
then A51: x <= b2 by A47, XXREAL_0:2;
( a2 < x & a1 <= a2 implies a1 < x ) by XXREAL_0:2;
then ( x in e1 & x in e2 ) by A12, A13, A14, A15, A47, A50, A51;
hence x in e1 /\ e2 by XBOOLE_0:def 4; :: thesis: verum

end;

hence for x being real number holds
( x in e1 /\ e2 iff ( a2 < x & x <= b1 ) ) by A49; :: thesis: verum

end;

e1 /\ e2 = E1 /\ E2 by A12, A13;
hence e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A47, A48; :: thesis: verum

end;

hence ( e1 /\ e2 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } or e1 /\ e2 in {{}} ) by A21, A28, A32, A37, A43; :: thesis: verum

end;

( a2 < b1 & b2 <= a1 implies e1 /\ e2 in {{}} )

proof

assume A52: ( a2 < b1 & b2 <= a1 ) ; :: thesis: e1 /\ e2 in {{}}
e1 /\ e2 c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in e1 /\ e2 or x in {} )
assume A53: x in e1 /\ e2 ; :: thesis: x in {}
then A54: ( x in e1 & x in e2 ) by XBOOLE_0:def 4;
reconsider x = x as real number by A12, A53;
( a1 < x & x <= b1 & a2 < x & x <= b2 ) by A12, A13, A14, A15, A54;
hence x in {} by A52, XXREAL_0:2; :: thesis: verum

end;

then e1 /\ e2 = {} ;
hence e1 /\ e2 in {{}} by TARSKI:def 1; :: thesis: verum

end;

hence e1 /\ e2 in {{}} \/ { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A16, A20, XBOOLE_0:def 3; :: thesis: verum

end;

hence e1 /\ e2 in S by A1; :: thesis: verum

end;

hence e1 /\ e2 in S by A6, A7, A8, A9, TARSKI:def 1; :: thesis: verum

end;

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: ( not S3 \ S4 is empty implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )
assume A55: not S3 \ S4 is empty ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
A57: not S3 in {{}} by A55, TARSKI:def 1;
A58: ( S4 in {{}} or S4 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ) by A1, XBOOLE_0:def 3;
A59: ( S4 = {} implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume A60: S4 = {} ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
A61: {S3} c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {S3} or x in S )
assume x in {S3} ; :: thesis: x in S
then x is Element of S by TARSKI:def 1;
hence x in S by A2, SUBSET_1:def 1; :: thesis: verum

end;

{S3} is a_partition of S3 by A55, EQREL_1:39;
hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A60, A61; :: thesis: verum

end;

( S4 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume A62: S4 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
S3 in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A1, A57, XBOOLE_0:def 3;
then consider E1 being Subset of REAL such that
A63: ( S3 = E1 & ex a1, b1 being Real st
( a1 < b1 & ( for x being real number holds
( x in E1 iff ( a1 < x & x <= b1 ) ) ) ) ) ;
consider E2 being Subset of REAL such that
A64: ( S4 = E2 & ex a2, b2 being Real st
( a2 < b2 & ( for x being real number holds
( x in E2 iff ( a2 < x & x <= b2 ) ) ) ) ) by A62;
consider a1, b1 being Real such that
A65: ( a1 < b1 & ( for x being real number holds
( x in E1 iff ( a1 < x & x <= b1 ) ) ) ) by A63;
consider a2, b2 being Real such that
A66: ( a2 < b2 & ( for x being real number holds
( x in E2 iff ( a2 < x & x <= b2 ) ) ) ) by A64;
A67: for x being real number holds
( x in S3 \ S4 iff ( a1 < x & x <= b1 & ( not a2 < x or not x <= b2 ) ) )

proof

A68: for x being real number st x in S3 \ S4 holds
( a1 < x & x <= b1 & ( not a2 < x or not x <= b2 ) )

proof

let x be real number ; :: thesis: ( x in S3 \ S4 implies ( a1 < x & x <= b1 & ( not a2 < x or not x <= b2 ) ) )
assume x in S3 \ S4 ; :: thesis: ( a1 < x & x <= b1 & ( not a2 < x or not x <= b2 ) )
then ( x in S3 & not x in S4 ) by XBOOLE_0:def 5;
hence ( a1 < x & x <= b1 & ( not a2 < x or not x <= b2 ) ) by A63, A64, A65, A66; :: thesis: verum

end;

for x being real number st a1 < x & x <= b1 & ( not a2 < x or not x <= b2 ) holds
x in S3 \ S4

proof

let x be real number ; :: thesis: ( a1 < x & x <= b1 & ( not a2 < x or not x <= b2 ) implies x in S3 \ S4 )
assume ( a1 < x & x <= b1 & ( not a2 < x or not x <= b2 ) ) ; :: thesis: x in S3 \ S4
then ( x in S3 & not x in S4 ) by A63, A64, A65, A66;
hence x in S3 \ S4 by XBOOLE_0:def 5; :: thesis: verum

end;

hence for x being real number holds
( x in S3 \ S4 iff ( a1 < x & x <= b1 & ( not a2 < x or not x <= b2 ) ) ) by A68; :: thesis: verum

end;

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

proof

assume A70: ( a1 < b1 & a2 < b2 & b1 <= a2 & b1 <= b2 ) ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
A71: S3 \ S4 = S3

proof

S3 c= S3 \ S4

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S3 or x in S3 \ S4 )
assume A72: x in S3 ; :: thesis: x in S3 \ S4
then reconsider x = x as real number by A63;
( a1 < x & x <= b1 ) by A63, A65, A72;
then ( a1 < x & x <= b1 & ( not a2 < x or not x <= b2 ) ) by A70, XXREAL_0:2;
hence x in S3 \ S4 by A67; :: thesis: verum

end;

hence S3 \ S4 = S3 ; :: thesis: verum

end;

A72a: {S3} c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {S3} or x in S )
assume x in {S3} ; :: thesis: x in S
then x is Element of S by TARSKI:def 1;
hence x in S by A2, SUBSET_1:def 1; :: thesis: verum

end;

{S3} is a_partition of S3 by A55, EQREL_1:39;
hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A71, A72a; :: thesis: verum

end;

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

proof

assume A75: ( a1 < b1 & a2 < b2 & a2 < b1 & a1 <= a2 & b1 <= b2 ) ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
A76: ( a1 < b1 & a2 < b2 & a2 < b1 & a1 = a2 & b1 <= b2 implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume A77: ( a1 < b1 & a2 < b2 & a2 < b1 & a1 = a2 & b1 <= b2 ) ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
S3 \ S4 c= {}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S3 \ S4 or y in {} )
assume A78: y in S3 \ S4 ; :: thesis: y in {}
then reconsider y = y as real number by A63;
( a1 < y & y <= b1 & ( y <= a2 or b2 < y ) ) by A67, A78;
hence y in {} by A77, XXREAL_0:2; :: thesis: verum

end;

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

end;

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

proof

assume A79: ( a1 < b1 & a2 < b2 & a2 < b1 & a1 < a2 & b1 <= b2 ) ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
set P = { x where x is real number : ( a1 < x & x <= a2 ) } ;
A80: S3 \ S4 = { x where x is real number : ( a1 < x & x <= a2 ) }

proof

A81: S3 \ S4 c= { x where x is real number : ( a1 < x & x <= a2 ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S3 \ S4 or y in { x where x is real number : ( a1 < x & x <= a2 ) } )
assume A82: y in S3 \ S4 ; :: thesis: y in { x where x is real number : ( a1 < x & x <= a2 ) }
then reconsider y = y as real number by A63;
( a1 < y & y <= b1 & ( y <= a2 or b2 < y ) ) by A67, A82;
hence y in { x where x is real number : ( a1 < x & x <= a2 ) } by A79, XXREAL_0:2; :: thesis: verum

end;

{ x where x is real number : ( a1 < x & x <= a2 ) } c= S3 \ S4

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is real number : ( a1 < x & x <= a2 ) } or y in S3 \ S4 )
assume y in { x where x is real number : ( a1 < x & x <= a2 ) } ; :: thesis: y in S3 \ S4
then consider y0 being real number such that
A83: ( y = y0 & a1 < y0 & y0 <= a2 ) ;
( a1 < y0 & y0 <= b1 & ( y0 <= a2 or b2 < y0 ) ) by A79, A83, XXREAL_0:2;
hence y in S3 \ S4 by A67, A83; :: thesis: verum

end;

hence S3 \ S4 = { x where x is real number : ( a1 < x & x <= a2 ) } by A81; :: thesis: verum

end;

A83a: { { x where x is real number : ( a1 < x & x <= a2 ) } } c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { { x where x is real number : ( a1 < x & x <= a2 ) } } or x in S )
assume x in { { x where x is real number : ( a1 < x & x <= a2 ) } } ; :: thesis: x in S
then A84: x = { x where x is real number : ( a1 < x & x <= a2 ) } by TARSKI:def 1;
{ x where x is real number : ( a1 < x & x <= a2 ) } in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }

proof

A86: { x where x is real number : ( a1 < x & x <= a2 ) } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is real number : ( a1 < x & x <= a2 ) } or x in REAL )
assume x in { x where x is real number : ( a1 < x & x <= a2 ) } ; :: thesis: x in REAL
then consider x0 being real number such that
A87: ( x = x0 & a1 < x0 & x0 <= a2 ) ;
thus x in REAL by A87, XREAL_0:def 1; :: thesis: verum

end;

for x being real number holds
( x in { x where x is real number : ( a1 < x & x <= a2 ) } iff ( a1 < x & x <= a2 ) )

proof

for x being real number st x in { x where x is real number : ( a1 < x & x <= a2 ) } holds
( a1 < x & x <= a2 )

proof

let x be real number ; :: thesis: ( x in { x where x is real number : ( a1 < x & x <= a2 ) } implies ( a1 < x & x <= a2 ) )
assume x in { x where x is real number : ( a1 < x & x <= a2 ) } ; :: thesis: ( a1 < x & x <= a2 )
then consider x0 being real number such that
A89: ( x = x0 & a1 < x0 & x0 <= a2 ) ;
thus ( a1 < x & x <= a2 ) by A89; :: thesis: verum

end;

hence for x being real number holds
( x in { x where x is real number : ( a1 < x & x <= a2 ) } iff ( a1 < x & x <= a2 ) ) ; :: thesis: verum

end;

hence { x where x is real number : ( a1 < x & x <= a2 ) } in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A79, A86; :: thesis: verum

end;

hence x in S by A1, A84, XBOOLE_0:def 3; :: thesis: verum

end;

{ { x where x is real number : ( a1 < x & x <= a2 ) } } is a_partition of { x where x is real number : ( a1 < x & x <= a2 ) } by A80, A55, EQREL_1:39;
hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A80, A83a; :: thesis: verum

end;

hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A75, A76, XXREAL_0:1; :: thesis: verum

end;

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

proof

assume A91: ( a1 < b1 & a2 < b2 & a2 < b1 & a1 <= a2 & b2 < b1 & a1 < b2 ) ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
A92: ( a1 < b1 & a2 < b2 & a2 < b1 & a1 < a2 & b2 < b1 & a1 < b2 implies ex z being finite Subset of S st z is a_partition of S3 \ S4 )

proof

assume A93: ( a1 < b1 & a2 < b2 & a2 < b1 & a1 < a2 & b2 < b1 & a1 < b2 ) ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
set P1 = { x where x is Real : ( a1 < x & x <= a2 ) } ;
A94: { x where x is Real : ( a1 < x & x <= a2 ) } in S

proof

{ x where x is Real : ( a1 < x & x <= a2 ) } in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }

proof

{ x where x is Real : ( a1 < x & x <= a2 ) } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Real : ( a1 < x & x <= a2 ) } or x in REAL )
assume x in { x where x is Real : ( a1 < x & x <= a2 ) } ; :: thesis: x in REAL
then consider x0 being Real such that
A96: ( x = x0 & a1 < x0 & x0 <= a2 ) ;
thus x in REAL by A96, XREAL_0:def 1; :: thesis: verum

end;

then A95: { x where x is Real : ( a1 < x & x <= a2 ) } is Subset of REAL ;
for x being real number holds
( x in { x where x is Real : ( a1 < x & x <= a2 ) } iff ( a1 < x & x <= a2 ) )

proof

for x being real number st x in { x where x is Real : ( a1 < x & x <= a2 ) } holds
( a1 < x & x <= a2 )

proof

let x be real number ; :: thesis: ( x in { x where x is Real : ( a1 < x & x <= a2 ) } implies ( a1 < x & x <= a2 ) )
assume x in { x where x is Real : ( a1 < x & x <= a2 ) } ; :: thesis: ( a1 < x & x <= a2 )
then consider x0 being Real such that
A97: ( x = x0 & a1 < x0 & x0 <= a2 ) ;
thus ( a1 < x & x <= a2 ) by A97; :: thesis: verum

end;

hence for x being real number holds
( x in { x where x is Real : ( a1 < x & x <= a2 ) } iff ( a1 < x & x <= a2 ) ) ; :: thesis: verum

end;

hence { x where x is Real : ( a1 < x & x <= a2 ) } in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A93, A95; :: thesis: verum

end;

hence { x where x is Real : ( a1 < x & x <= a2 ) } in S by A1, XBOOLE_0:def 3; :: thesis: verum

end;

set P2 = { x where x is Real : ( b2 < x & x <= b1 ) } ;
A98: { x where x is Real : ( b2 < x & x <= b1 ) } in S

proof

{ x where x is Real : ( b2 < x & x <= b1 ) } in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }

proof

A99: { x where x is Real : ( b2 < x & x <= b1 ) } is Subset of REAL

proof

{ x where x is Real : ( b2 < x & x <= b1 ) } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Real : ( b2 < x & x <= b1 ) } or x in REAL )
assume x in { x where x is Real : ( b2 < x & x <= b1 ) } ; :: thesis: x in REAL
then consider x0 being Real such that
A100: ( x = x0 & b2 < x0 & x0 <= b1 ) ;
thus x in REAL by A100, XREAL_0:def 1; :: thesis: verum

end;

hence { x where x is Real : ( b2 < x & x <= b1 ) } is Subset of REAL ; :: thesis: verum

end;

for x being real number holds
( x in { x where x is Real : ( b2 < x & x <= b1 ) } iff ( b2 < x & x <= b1 ) )

proof

for x being real number st x in { x where x is Real : ( b2 < x & x <= b1 ) } holds
( b2 < x & x <= b1 )

proof

let x be real number ; :: thesis: ( x in { x where x is Real : ( b2 < x & x <= b1 ) } implies ( b2 < x & x <= b1 ) )
assume x in { x where x is Real : ( b2 < x & x <= b1 ) } ; :: thesis: ( b2 < x & x <= b1 )
then consider x0 being Real such that
A101: ( x = x0 & b2 < x0 & x0 <= b1 ) ;
thus ( b2 < x & x <= b1 ) by A101; :: thesis: verum

end;

hence for x being real number holds
( x in { x where x is Real : ( b2 < x & x <= b1 ) } iff ( b2 < x & x <= b1 ) ) ; :: thesis: verum

end;

hence { x where x is Real : ( b2 < x & x <= b1 ) } in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A93, A99; :: thesis: verum

end;

hence { x where x is Real : ( b2 < x & x <= b1 ) } in S by A1, XBOOLE_0:def 3; :: thesis: verum

end;

A101a: { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } c= S by A94, A98, TARSKI:def 2;
A102: { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } is Subset-Family of (S3 \ S4)

proof

{ { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } c= bool (S3 \ S4)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } or x in bool (S3 \ S4) )
assume A103: x in { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } ; :: thesis: x in bool (S3 \ S4)
A104: { x where x is Real : ( a1 < x & x <= a2 ) } in bool (S3 \ S4)

proof

{ x where x is Real : ( a1 < x & x <= a2 ) } c= S3 \ S4

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Real : ( a1 < x & x <= a2 ) } or x in S3 \ S4 )
assume x in { x where x is Real : ( a1 < x & x <= a2 ) } ; :: thesis: x in S3 \ S4
then consider x0 being Real such that
A105: ( x = x0 & a1 < x0 & x0 <= a2 ) ;
reconsider x = x as real number by A105, TARSKI:1;
( a1 < x & x <= a2 & x <= b1 ) by A93, A105, XXREAL_0:2;
hence x in S3 \ S4 by A67; :: thesis: verum

end;

hence { x where x is Real : ( a1 < x & x <= a2 ) } in bool (S3 \ S4) ; :: thesis: verum

end;

{ x where x is Real : ( b2 < x & x <= b1 ) } in bool (S3 \ S4)

proof

{ x where x is Real : ( b2 < x & x <= b1 ) } c= S3 \ S4

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Real : ( b2 < x & x <= b1 ) } or x in S3 \ S4 )
assume x in { x where x is Real : ( b2 < x & x <= b1 ) } ; :: thesis: x in S3 \ S4
then consider x0 being Real such that
A106: ( x = x0 & b2 < x0 & x0 <= b1 ) ;
reconsider x = x as real number by A106, TARSKI:1;
( a1 < x & b2 < x & x <= b1 ) by A93, A106, XXREAL_0:2;
hence x in S3 \ S4 by A67; :: thesis: verum

end;

hence { x where x is Real : ( b2 < x & x <= b1 ) } in bool (S3 \ S4) ; :: thesis: verum

end;

hence x in bool (S3 \ S4) by A103, A104, TARSKI:def 2; :: thesis: verum

end;

hence { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } is Subset-Family of (S3 \ S4) ; :: thesis: verum

end;

A107: union { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } = S3 \ S4

proof

A108: union { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } = { x where x is Real : ( a1 < x & x <= a2 ) } \/ { x where x is Real : ( b2 < x & x <= b1 ) } by ZFMISC_1:75;
A109: { x where x is Real : ( a1 < x & x <= a2 ) } \/ { x where x is Real : ( b2 < x & x <= b1 ) } c= S3 \ S4

proof

union { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } c= union (bool (S3 \ S4)) by A102, ZFMISC_1:77;
hence { x where x is Real : ( a1 < x & x <= a2 ) } \/ { x where x is Real : ( b2 < x & x <= b1 ) } c= S3 \ S4 by A108, ZFMISC_1:81; :: thesis: verum

end;

S3 \ S4 c= { x where x is Real : ( a1 < x & x <= a2 ) } \/ { x where x is Real : ( b2 < x & x <= b1 ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S3 \ S4 or y in { x where x is Real : ( a1 < x & x <= a2 ) } \/ { x where x is Real : ( b2 < x & x <= b1 ) } )
assume A110: y in S3 \ S4 ; :: thesis: y in { x where x is Real : ( a1 < x & x <= a2 ) } \/ { x where x is Real : ( b2 < x & x <= b1 ) }
then reconsider y = y as real number by A63;
( ( a1 < y & y <= a2 ) or ( b2 < y & y <= b1 ) ) by A67, A110;
then ( y in { x where x is Real : ( a1 < x & x <= a2 ) } or y in { x where x is Real : ( b2 < x & x <= b1 ) } ) ;
hence y in { x where x is Real : ( a1 < x & x <= a2 ) } \/ { x where x is Real : ( b2 < x & x <= b1 ) } by XBOOLE_0:def 3; :: thesis: verum

end;

hence union { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } = S3 \ S4 by ZFMISC_1:75, A109; :: thesis: verum

end;

for A being Subset of (S3 \ S4) st A in { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } holds
( A <> {} & ( for B being Subset of (S3 \ S4) holds
( not B in { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } or A = B or A misses B ) ) )

proof

let A be Subset of (S3 \ S4); :: thesis: ( A in { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } implies ( A <> {} & ( for B being Subset of (S3 \ S4) holds
( not B in { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } or A = B or A misses B ) ) ) )
assume A111: A in { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } ; :: thesis: ( A <> {} & ( for B being Subset of (S3 \ S4) holds
( not B in { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } or A = B or A misses B ) ) )
A112: { x where x is Real : ( a1 < x & x <= a2 ) } <> {}

proof

a2 in { x where x is Real : ( a1 < x & x <= a2 ) } by A93;
hence { x where x is Real : ( a1 < x & x <= a2 ) } <> {} ; :: thesis: verum

end;

A113: { x where x is Real : ( b2 < x & x <= b1 ) } <> {}

proof

b1 in { x where x is Real : ( b2 < x & x <= b1 ) } by A93;
hence { x where x is Real : ( b2 < x & x <= b1 ) } <> {} ; :: thesis: verum

end;

for B being Subset of (S3 \ S4) holds
( not B in { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } or A = B or A misses B )

proof

let B be Subset of (S3 \ S4); :: thesis: ( not B in { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } or A = B or A misses B )
assume B in { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } ; :: thesis: ( A = B or A misses B )
then A114: ( ( A = { x where x is Real : ( a1 < x & x <= a2 ) } & B = { x where x is Real : ( a1 < x & x <= a2 ) } ) or ( A = { x where x is Real : ( a1 < x & x <= a2 ) } & B = { x where x is Real : ( b2 < x & x <= b1 ) } ) or ( A = { x where x is Real : ( b2 < x & x <= b1 ) } & B = { x where x is Real : ( a1 < x & x <= a2 ) } ) or ( A = { x where x is Real : ( b2 < x & x <= b1 ) } & B = { x where x is Real : ( b2 < x & x <= b1 ) } ) ) by A111, TARSKI:def 2;
{ x where x is Real : ( a1 < x & x <= a2 ) } misses { x where x is Real : ( b2 < x & x <= b1 ) }

proof

{ x where x is Real : ( a1 < x & x <= a2 ) } /\ { x where x is Real : ( b2 < x & x <= b1 ) } c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Real : ( a1 < x & x <= a2 ) } /\ { x where x is Real : ( b2 < x & x <= b1 ) } or x in {} )
assume x in { x where x is Real : ( a1 < x & x <= a2 ) } /\ { x where x is Real : ( b2 < x & x <= b1 ) } ; :: thesis: x in {}
then A115: ( x in { x where x is Real : ( a1 < x & x <= a2 ) } & x in { x where x is Real : ( b2 < x & x <= b1 ) } ) by XBOOLE_0:def 4;
then consider x0 being Real such that
A116: ( x = x0 & a1 < x0 & x0 <= a2 ) ;
consider y0 being Real such that
A117: ( x = y0 & b2 < y0 & y0 <= b1 ) by A115;
thus x in {} by A93, A116, A117, XXREAL_0:2; :: thesis: verum

end;

hence { x where x is Real : ( a1 < x & x <= a2 ) } misses { x where x is Real : ( b2 < x & x <= b1 ) } ; :: thesis: verum

end;

hence ( A = B or A misses B ) by A114; :: thesis: verum

end;

hence ( A <> {} & ( for B being Subset of (S3 \ S4) holds
( not B in { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } or A = B or A misses B ) ) ) by A111, A112, A113; :: thesis: verum

end;

then { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } is a_partition of S3 \ S4 by A102, A107, EQREL_1:def 4;
hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A101a; :: thesis: verum

end;

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

proof

assume A118: ( a1 < b1 & a2 < b2 & a2 < b1 & a1 = a2 & b2 < b1 & a1 < b2 ) ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
set P = { x where x is real number : ( b2 < x & x <= b1 ) } ;
A119: S3 \ S4 = { x where x is real number : ( b2 < x & x <= b1 ) }

proof

A120: S3 \ S4 c= { x where x is real number : ( b2 < x & x <= b1 ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S3 \ S4 or y in { x where x is real number : ( b2 < x & x <= b1 ) } )
assume A121: y in S3 \ S4 ; :: thesis: y in { x where x is real number : ( b2 < x & x <= b1 ) }
then reconsider y = y as real number by A63;
( a1 < y & y <= b1 & ( not a2 < y or not y <= b2 ) ) by A67, A121;
hence y in { x where x is real number : ( b2 < x & x <= b1 ) } by A118; :: thesis: verum

end;

{ x where x is real number : ( b2 < x & x <= b1 ) } c= S3 \ S4

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is real number : ( b2 < x & x <= b1 ) } or y in S3 \ S4 )
assume y in { x where x is real number : ( b2 < x & x <= b1 ) } ; :: thesis: y in S3 \ S4
then consider y0 being real number such that
A122: ( y = y0 & b2 < y0 & y0 <= b1 ) ;
( a1 < y0 & y0 <= b1 & ( y0 <= a2 or b2 < y0 ) ) by A118, A122, XXREAL_0:2;
hence y in S3 \ S4 by A67, A122; :: thesis: verum

end;

hence S3 \ S4 = { x where x is real number : ( b2 < x & x <= b1 ) } by A120; :: thesis: verum

end;

A123: { { x where x is real number : ( b2 < x & x <= b1 ) } } c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { { x where x is real number : ( b2 < x & x <= b1 ) } } or x in S )
assume x in { { x where x is real number : ( b2 < x & x <= b1 ) } } ; :: thesis: x in S
then A124: x = { x where x is real number : ( b2 < x & x <= b1 ) } by TARSKI:def 1;
{ x where x is real number : ( b2 < x & x <= b1 ) } in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }

proof

A125: { x where x is real number : ( b2 < x & x <= b1 ) } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is real number : ( b2 < x & x <= b1 ) } or x in REAL )
assume x in { x where x is real number : ( b2 < x & x <= b1 ) } ; :: thesis: x in REAL
then consider x0 being real number such that
A126: ( x = x0 & b2 < x0 & x0 <= b1 ) ;
thus x in REAL by A126, XREAL_0:def 1; :: thesis: verum

end;

for x being real number holds
( x in { x where x is real number : ( b2 < x & x <= b1 ) } iff ( b2 < x & x <= b1 ) )

proof

for x being real number st x in { x where x is real number : ( b2 < x & x <= b1 ) } holds
( b2 < x & x <= b1 )

proof

let x be real number ; :: thesis: ( x in { x where x is real number : ( b2 < x & x <= b1 ) } implies ( b2 < x & x <= b1 ) )
assume x in { x where x is real number : ( b2 < x & x <= b1 ) } ; :: thesis: ( b2 < x & x <= b1 )
then consider x0 being real number such that
A126a: ( x = x0 & b2 < x0 & x0 <= b1 ) ;
thus ( b2 < x & x <= b1 ) by A126a; :: thesis: verum

end;

hence for x being real number holds
( x in { x where x is real number : ( b2 < x & x <= b1 ) } iff ( b2 < x & x <= b1 ) ) ; :: thesis: verum

end;

hence { x where x is real number : ( b2 < x & x <= b1 ) } in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A118, A125; :: thesis: verum

end;

hence x in S by A1, A124, XBOOLE_0:def 3; :: thesis: verum

end;

{ { x where x is real number : ( b2 < x & x <= b1 ) } } is a_partition of { x where x is real number : ( b2 < x & x <= b1 ) } by A55, A119, EQREL_1:39;
hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A123, A119; :: thesis: verum

end;

hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A91, A92, XXREAL_0:1; :: thesis: verum

end;

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

proof

assume A128: ( a1 < b1 & a2 < b2 & b1 <= b2 & a2 < b1 & a2 < a1 ) ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
S3 \ S4 c= {}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S3 \ S4 or y in {} )
assume A129: y in S3 \ S4 ; :: thesis: y in {}
then reconsider y = y as real number by A63;
A130: ( a1 < y & y <= b1 & ( y <= a2 or b2 < y ) ) by A67, A129;
thus y in {} by A128, A130, XXREAL_0:2; :: thesis: verum

end;

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

end;

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

proof

assume A132: ( a1 < b1 & a2 < b2 & b2 < b1 & b2 <= a1 & a2 < b1 & a2 < a1 ) ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
S3 c= S3 \ S4

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S3 or x in S3 \ S4 )
assume A133: x in S3 ; :: thesis: x in S3 \ S4
then reconsider x = x as real number by A63;
A134: ( a1 < x & x <= b1 ) by A63, A65, A133;
b2 < x by A132, A134, XXREAL_0:2;
hence x in S3 \ S4 by A67, A134; :: thesis: verum

end;

then A135: S3 = S3 \ S4 ;
A135a: {S3} c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {S3} or x in S )
assume x in {S3} ; :: thesis: x in S
then x is Element of S by TARSKI:def 1;
hence x in S by A2, SUBSET_1:def 1; :: thesis: verum

end;

{S3} is a_partition of S3 by A55, EQREL_1:39;
hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A135a, A135; :: thesis: verum

end;

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

proof

assume A137: ( a1 < b1 & a2 < b2 & b2 < b1 & a1 < b2 & a2 < b1 & a2 < a1 ) ; :: thesis: ex z being finite Subset of S st z is a_partition of S3 \ S4
set P = { x where x is real number : ( b2 < x & x <= b1 ) } ;
A138: S3 \ S4 = { x where x is real number : ( b2 < x & x <= b1 ) }

proof

A139: S3 \ S4 c= { x where x is real number : ( b2 < x & x <= b1 ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S3 \ S4 or y in { x where x is real number : ( b2 < x & x <= b1 ) } )
assume A140: y in S3 \ S4 ; :: thesis: y in { x where x is real number : ( b2 < x & x <= b1 ) }
then reconsider y = y as real number by A63;
( ( a1 < y & y <= b1 & y <= a2 ) or ( a1 < y & y <= b1 & b2 < y ) ) by A67, A140;
hence y in { x where x is real number : ( b2 < x & x <= b1 ) } by A137, XXREAL_0:2; :: thesis: verum

end;

{ x where x is real number : ( b2 < x & x <= b1 ) } c= S3 \ S4

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is real number : ( b2 < x & x <= b1 ) } or y in S3 \ S4 )
assume y in { x where x is real number : ( b2 < x & x <= b1 ) } ; :: thesis: y in S3 \ S4
then consider y0 being real number such that
A141: ( y = y0 & b2 < y0 & y0 <= b1 ) ;
( a1 < y0 & y0 <= b1 & ( y0 <= a2 or b2 < y0 ) ) by A137, A141, XXREAL_0:2;
hence y in S3 \ S4 by A67, A141; :: thesis: verum

end;

hence S3 \ S4 = { x where x is real number : ( b2 < x & x <= b1 ) } by A139; :: thesis: verum

end;

A142: { { x where x is real number : ( b2 < x & x <= b1 ) } } c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { { x where x is real number : ( b2 < x & x <= b1 ) } } or x in S )
assume x in { { x where x is real number : ( b2 < x & x <= b1 ) } } ; :: thesis: x in S
then A143: x = { x where x is real number : ( b2 < x & x <= b1 ) } by TARSKI:def 1;
{ x where x is real number : ( b2 < x & x <= b1 ) } in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) }

proof

A144: { x where x is real number : ( b2 < x & x <= b1 ) } is Subset of REAL

proof

{ x where x is real number : ( b2 < x & x <= b1 ) } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is real number : ( b2 < x & x <= b1 ) } or x in REAL )
assume x in { x where x is real number : ( b2 < x & x <= b1 ) } ; :: thesis: x in REAL
then consider x0 being real number such that
A145: ( x = x0 & b2 < x0 & x0 <= b1 ) ;
thus x in REAL by A145, XREAL_0:def 1; :: thesis: verum

end;

hence { x where x is real number : ( b2 < x & x <= b1 ) } is Subset of REAL ; :: thesis: verum

end;

for x being real number holds
( x in { x where x is real number : ( b2 < x & x <= b1 ) } iff ( b2 < x & x <= b1 ) )

proof

for x being real number st x in { x where x is real number : ( b2 < x & x <= b1 ) } holds
( b2 < x & x <= b1 )

proof

let x be real number ; :: thesis: ( x in { x where x is real number : ( b2 < x & x <= b1 ) } implies ( b2 < x & x <= b1 ) )
assume x in { x where x is real number : ( b2 < x & x <= b1 ) } ; :: thesis: ( b2 < x & x <= b1 )
then consider x0 being real number such that
A146: ( x = x0 & b2 < x0 & x0 <= b1 ) ;
thus ( b2 < x & x <= b1 ) by A146; :: thesis: verum

end;

hence for x being real number holds
( x in { x where x is real number : ( b2 < x & x <= b1 ) } iff ( b2 < x & x <= b1 ) ) ; :: thesis: verum

end;

hence { x where x is real number : ( b2 < x & x <= b1 ) } in { s where s is Subset of REAL : ex a, b being Real st
( a < b & ( for x being real number holds
( x in s iff ( a < x & x <= b ) ) ) ) } by A137, A144; :: thesis: verum

end;

hence x in S by A1, A143, XBOOLE_0:def 3; :: thesis: verum

end;

{ { x where x is real number : ( b2 < x & x <= b1 ) } } is a_partition of { x where x is real number : ( b2 < x & x <= b1 ) } by A55, A138, EQREL_1:39;
hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A142, A138; :: thesis: verum

end;

hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A65, A66, A69, A74, A90, A127, A131, XXREAL_0:2; :: thesis: verum

end;

hence ex z being finite Subset of S st z is a_partition of S3 \ S4 by A58, A59, TARSKI:def 1; :: thesis: verum

end;

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

end;

hence ( S is cap-closed & S is diff-finite-partition-closed with_empty_element Subset-Family of REAL ) by A2, A3; :: thesis: verum