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))

c in Intersection (half_open_sets (a,b))

( 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

A1: for c being set st not c in [.a,b.] holds

not c in Intersection (half_open_sets (a,b))

proof

A11:
for c being set st c in [.a,b.] holds
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))

end;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;

end;

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 )

end;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;( not c = q or not a <= c or not c <= b ) by A4;

hence ( a > c or c > b ) ; :: thesis: verum

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

end;

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

end;proof

hence
not c in Intersection (half_open_sets (a,b))
by PROB_1:13; :: thesis: verum
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;( 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

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 )

end;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

hence
not c in Intersection (half_open_sets (a,b))
by A8; :: thesis: verum
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;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

c in Intersection (half_open_sets (a,b))

proof

for c being object holds
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 )

end;( c in [.a,b.] implies for n being Nat holds c in (half_open_sets (a,b)) . n )

proof

hence
( c in [.a,b.] implies c in Intersection (half_open_sets (a,b)) )
by PROB_1:13; :: thesis: verum
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

end;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
end;

hence
c in (half_open_sets (a,b)) . n
by A12; :: thesis: verumper cases
( n = 0 or n > 0 )
;

end;

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

(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: verum

end;hence [.a,b.] c= (half_open_sets (a,b)) . n by A14, A13, XXREAL_1:43; :: thesis: verum

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;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

( 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