let a, b be real number ; :: thesis: Intersection (half_open_sets (a,b)) = [.a,b.]
SP1: 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 J0: 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 J0;

suppose not c in REAL ; :: thesis: not c in Intersection (half_open_sets (a,b))

hence not c in Intersection (half_open_sets (a,b)) ; :: thesis: verum

end;

suppose SJ0: ( 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 ;
SJ2: not c in { q where q is Element of ExtREAL : ( a <= q & q <= b ) } by SJ0, XXREAL_1:def 1;
SJ3: ( 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 SJ2;
hence ( a > c or c > b ) ; :: thesis: verum

end;

per cases ( a > c or c > b ) by SJ3;

suppose QQ0: 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 Def3;
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 QQ0; :: 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 Element of NAT such that
FF1: ( 1 / n < c - b & n > 0 ) by FRECHET:36, XREAL_1:50;
FF2: (1 / n) + b < (c - b) + b by FF1, 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 Def3;
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
QQ0: ( 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 QQ2: a / (n + 1) < a / n by FF1, XREAL_1:106;
b + (1 / (n + 1)) < b + (1 / n) by QQ2, XREAL_1:6;
hence not b + (1 / n) < c by QQ0, XXREAL_0:2; :: thesis: verum

end;

hence not c in Intersection (half_open_sets (a,b)) by FF2; :: thesis: verum

end;

end;

end;

end;

end;

SP0: 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 Element of NAT holds c in (half_open_sets (a,b)) . n )

proof

assume AJ0: c in [.a,b.] ; :: thesis: for n being Element of NAT holds c in (half_open_sets (a,b)) . n
let n be Element of NAT ; :: thesis: c in (half_open_sets (a,b)) . n
AAJ1: 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 AT0: n = 0 ; :: thesis: [.a,b.] c= (half_open_sets (a,b)) . n

(half_open_sets (a,b)) . 0 = halfline_fin (a,(b + 1)) by Def3;
hence [.a,b.] c= (half_open_sets (a,b)) . n by AT0, AAJ1, XXREAL_1:43; :: thesis: verum

end;

suppose n > 0 ; :: thesis: [.a,b.] c= (half_open_sets (a,b)) . n

then consider k being Nat such that
TT0: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
TT2: (half_open_sets (a,b)) . (k + 1) = halfline_fin (a,(b + (1 / (k + 1)))) by Def3;
b < b + (1 / n) by TT0, XREAL_1:29;
hence [.a,b.] c= (half_open_sets (a,b)) . n by TT2, TT0, XXREAL_1:43; :: thesis: verum

end;

end;

end;

hence c in (half_open_sets (a,b)) . n by AJ0; :: 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 set holds
( c in Intersection (half_open_sets (a,b)) iff c in [.a,b.] ) by SP0, SP1;
hence Intersection (half_open_sets (a,b)) = [.a,b.] by TARSKI:1; :: thesis: verum