let S be Subset-Family of REAL; ( 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 ) ) ) ) }
; ( S is cap-closed & S is diff-finite-partition-closed with_empty_element Subset-Family of REAL )
A2:
S is with_empty_element
A3:
S is cap-closed
proof
let e1,
e2 be
set ;
FINSUB_1:def 2 ( not e1 in S or not e2 in S or e1 /\ e2 in S )
assume A4:
e1 in S
;
( not e2 in S or e1 /\ e2 in S )
assume A5:
e2 in S
;
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 )
A9:
(
e2 = {} implies
e1 /\ e2 in S )
(
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 ) ) ) ) }
;
( 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 ) ) ) ) }
;
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 {{}} )
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 )
;
( 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 ) ) ) ) } )
A28:
(
a2 < a1 &
b2 < b1 & not
a1 < b2 implies
e1 /\ e2 in {{}} )
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 ) ) ) ) } )
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 ) ) ) ) } )
A43:
(
a1 <= a2 &
b1 <= b2 & not
a2 < b1 implies
e1 /\ e2 in {{}} )
(
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 ) ) ) ) } )
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;
verum
end;
(
a2 < b1 &
b2 <= a1 implies
e1 /\ e2 in {{}} )
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;
verum
end;
hence
e1 /\ e2 in S
by A1;
verum
end;
hence
e1 /\ e2 in S
by A6, A7, A8, A9, TARSKI:def 1;
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;
( 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
;
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 )
(
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 ) ) ) ) }
;
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 ) )
for
x being
real number st
a1 < x &
x <= b1 & ( not
a2 < x or not
x <= b2 ) holds
x in S3 \ S4
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;
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 )
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 )
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 )
;
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 )
;
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
set P2 =
{ x where x is Real : ( b2 < x & x <= b1 ) } ;
A98:
{ x where x is Real : ( b2 < x & x <= b1 ) } in S
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)
A107:
union { { x where x is Real : ( a1 < x & x <= a2 ) } , { x where x is Real : ( b2 < x & x <= b1 ) } } = S3 \ S4
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);
( 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 ) } }
;
( 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 ) } <> {}
A113:
{ x where x is Real : ( b2 < x & x <= b1 ) } <> {}
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);
( 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 ) } }
;
( 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 ) }
hence
(
A = B or
A misses B )
by A114;
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;
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;
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 )
hence
ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4
by A91, A92, XXREAL_0:1;
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 )
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 )
(
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 )
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;
verum
end;
hence
ex
z being
finite Subset of
S st
z is
a_partition of
S3 \ S4
by A58, A59, TARSKI:def 1;
verum
end;
hence
S is
diff-finite-partition-closed
by SRINGS_1:def 2;
verum
end;
hence
( S is cap-closed & S is diff-finite-partition-closed with_empty_element Subset-Family of REAL )
by A2, A3; verum