let a, b be Real; :: thesis:
A1: for c being set st not c in [.a,b.] holds
not c in Intersection (half_open_sets (a,b))

let c be set ; :: thesis:
assume A2: not c in [.a,b.] ; :: thesis:

per cases by A2;

suppose not c in REAL ; :: thesis:

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

end;

suppose A3: ( c in REAL & not c in [.a,b.] ) ; :: thesis:

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 )

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:

end;

per cases by A5;

suppose A6: a > c ; :: thesis:

not for n being Element of NAT holds c in (half_open_sets (a,b)) . n

take n = 0 ; :: thesis:
( 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:

end;

hence not c in Intersection (half_open_sets (a,b)) by PROB_1:13; :: thesis:

end;

suppose c > b ; :: thesis:

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 )

assume c in Intersection (half_open_sets (a,b)) ; :: thesis:
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:

end;

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

end;

end;

end;

end;

end;

A11: for c being set st c in [.a,b.] holds
c in Intersection (half_open_sets (a,b))

let c be set ; :: thesis:
( c in [.a,b.] implies for n being Nat holds c in (half_open_sets (a,b)) . n )

assume A12: c in [.a,b.] ; :: thesis:
let n be Nat; :: thesis:
A13: b < b + 1 by XREAL_1:29;
[.a,b.] c= (half_open_sets (a,b)) . n

suppose A14: n = 0 ; :: thesis:

(half_open_sets (a,b)) . 0 = halfline_fin (a,(b + 1)) by Def1;
hence [.a,b.] c= (half_open_sets (a,b)) . n by A14, A13, XXREAL_1:43; :: thesis:

end;

suppose n > 0 ; :: thesis:

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:

end;

end;

end;

hence c in (half_open_sets (a,b)) . n by A12; :: thesis:

end;

hence ( c in [.a,b.] implies c in Intersection (half_open_sets (a,b)) ) by PROB_1:13; :: thesis:

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: