let a, b be Real; :: thesis: Intersection (half_open_sets (a,b)) = [.a,b.]
A1: for c being set st not c in [.a,b.] holds
not c in Intersection (half_open_sets (a,b))
proof
let c be set ; :: thesis: ( not c in [.a,b.] implies not c in Intersection (half_open_sets (a,b)) )
assume A2: not c in [.a,b.] ; :: thesis: not c in Intersection (half_open_sets (a,b))
per cases ( not c in REAL or ( c in REAL & not c in [.a,b.] ) ) by A2;
suppose A3: ( c in REAL & not c in [.a,b.] ) ; :: thesis: not c in Intersection (half_open_sets (a,b))
then reconsider c = c as Element of REAL ;
A4: not c in { q where q is Element of ExtREAL : ( a <= q & q <= b ) } by A3, XXREAL_1:def 1;
A5: ( a > c or c > b )
proof
reconsider q = c as Element of ExtREAL by XXREAL_0:def 1;
( not c = q or not a <= c or not c <= b ) by A4;
hence ( a > c or c > b ) ; :: thesis: verum
end;
per cases ( a > c or c > b ) by A5;
suppose A6: a > c ; :: thesis: not c in Intersection (half_open_sets (a,b))
not for n being Element of NAT holds c in (half_open_sets (a,b)) . n
proof
take n = 0 ; :: thesis: not c in (half_open_sets (a,b)) . n
( c in (half_open_sets (a,b)) . 0 implies c in halfline_fin (a,(b + 1)) ) by Def1;
then ( c in (half_open_sets (a,b)) . 0 implies c in { q where q is Element of ExtREAL : ( a <= q & q < b + 1 ) } ) by XXREAL_1:def 2;
then ex q being Element of ExtREAL st
( c in (half_open_sets (a,b)) . 0 implies ( c = q & a <= q & q < b + 1 ) ) ;
hence not c in (half_open_sets (a,b)) . n by A6; :: thesis: verum
end;
hence not c in Intersection (half_open_sets (a,b)) by PROB_1:13; :: thesis: verum
end;
suppose c > b ; :: thesis: not c in Intersection (half_open_sets (a,b))
then consider n being Nat such that
A7: ( 1 / n < c - b & n > 0 ) by FRECHET:36, XREAL_1:50;
A8: (1 / n) + b < (c - b) + b by A7, XREAL_1:6;
( c in Intersection (half_open_sets (a,b)) implies not b + (1 / n) < c )
proof
assume c in Intersection (half_open_sets (a,b)) ; :: thesis: not b + (1 / n) < c
then c in (half_open_sets (a,b)) . (n + 1) by PROB_1:13;
then c in [.a,(b + (1 / (n + 1))).[ by Def1;
then c in { q where q is Element of ExtREAL : ( a <= q & q < b + (1 / (n + 1)) ) } by XXREAL_1:def 2;
then consider q being Element of ExtREAL such that
A9: ( c = q & a <= q & q < b + (1 / (n + 1)) ) ;
reconsider a = 1 as Element of NAT ;
n * 1 < (n + 1) * 1 by NAT_1:13;
then A10: a / (n + 1) < a / n by A7, XREAL_1:106;
b + (1 / (n + 1)) < b + (1 / n) by A10, XREAL_1:6;
hence not b + (1 / n) < c by A9, XXREAL_0:2; :: thesis: verum
end;
hence not c in Intersection (half_open_sets (a,b)) by A8; :: thesis: verum
end;
end;
end;
end;
end;
A11: for c being set st c in [.a,b.] holds
c in Intersection (half_open_sets (a,b))
proof
let c be set ; :: thesis: ( c in [.a,b.] implies c in Intersection (half_open_sets (a,b)) )
( c in [.a,b.] implies for n being Nat holds c in (half_open_sets (a,b)) . n )
proof
assume A12: c in [.a,b.] ; :: thesis: for n being Nat holds c in (half_open_sets (a,b)) . n
let n be Nat; :: thesis: c in (half_open_sets (a,b)) . n
A13: b < b + 1 by XREAL_1:29;
[.a,b.] c= (half_open_sets (a,b)) . n
proof
per cases ( n = 0 or n > 0 ) ;
suppose n > 0 ; :: thesis: [.a,b.] c= (half_open_sets (a,b)) . n
then consider k being Nat such that
A15: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A16: (half_open_sets (a,b)) . (k + 1) = halfline_fin (a,(b + (1 / (k + 1)))) by Def1;
b < b + (1 / n) by A15, XREAL_1:29;
hence [.a,b.] c= (half_open_sets (a,b)) . n by A16, A15, XXREAL_1:43; :: thesis: verum
end;
end;
end;
hence c in (half_open_sets (a,b)) . n by A12; :: thesis: verum
end;
hence ( c in [.a,b.] implies c in Intersection (half_open_sets (a,b)) ) by PROB_1:13; :: thesis: verum
end;
for c being object holds
( c in Intersection (half_open_sets (a,b)) iff c in [.a,b.] ) by A11, A1;
hence Intersection (half_open_sets (a,b)) = [.a,b.] by TARSKI:2; :: thesis: verum