let r be Real; :: thesis: ( r >= 0 implies [.0,+infty.] \ [.0,r.[ = [.r,+infty.] )

assume A0: r >= 0 ; :: thesis: [.0,+infty.] \ [.0,r.[ = [.r,+infty.]

for x being object holds

( x in [.0,+infty.] \ [.0,r.[ iff x in [.r,+infty.] )

assume A0: r >= 0 ; :: thesis: [.0,+infty.] \ [.0,r.[ = [.r,+infty.]

for x being object holds

( x in [.0,+infty.] \ [.0,r.[ iff x in [.r,+infty.] )

proof

hence
[.0,+infty.] \ [.0,r.[ = [.r,+infty.]
; :: thesis: verum
let x be object ; :: thesis: ( x in [.0,+infty.] \ [.0,r.[ iff x in [.r,+infty.] )

thus ( x in [.0,+infty.] \ [.0,r.[ implies x in [.r,+infty.] ) :: thesis: ( x in [.r,+infty.] implies x in [.0,+infty.] \ [.0,r.[ )

then x in { w where w is Element of ExtREAL : ( r <= w & w <= +infty ) } by XXREAL_1:def 1;

then consider w being Element of ExtREAL such that

H1: ( w = x & w >= r & w <= +infty ) ;

reconsider x = x as Element of ExtREAL by H1;

H2: x in [.0,+infty.] by A0, XXREAL_1:1, H1;

not x in [.0,r.[ by XXREAL_1:3, H1;

hence x in [.0,+infty.] \ [.0,r.[ by H2, XBOOLE_0:def 5; :: thesis: verum

end;thus ( x in [.0,+infty.] \ [.0,r.[ implies x in [.r,+infty.] ) :: thesis: ( x in [.r,+infty.] implies x in [.0,+infty.] \ [.0,r.[ )

proof

assume
x in [.r,+infty.]
; :: thesis: x in [.0,+infty.] \ [.0,r.[
assume
x in [.0,+infty.] \ [.0,r.[
; :: thesis: x in [.r,+infty.]

then G1: ( x in [.0,+infty.] & not x in [.0,r.[ ) by XBOOLE_0:def 5;

then x in { w where w is Element of ExtREAL : ( 0 <= w & w <= +infty ) } by XXREAL_1:def 1;

then consider w being Element of ExtREAL such that

G2: ( x = w & 0 <= w & w <= +infty ) ;

G3: not w in { w where w is Element of ExtREAL : ( 0 <= w & w < r ) } by XXREAL_1:def 2, G1, G2;

( 0 > w or w >= r ) by G3;

hence x in [.r,+infty.] by XXREAL_1:1, G2; :: thesis: verum

end;then G1: ( x in [.0,+infty.] & not x in [.0,r.[ ) by XBOOLE_0:def 5;

then x in { w where w is Element of ExtREAL : ( 0 <= w & w <= +infty ) } by XXREAL_1:def 1;

then consider w being Element of ExtREAL such that

G2: ( x = w & 0 <= w & w <= +infty ) ;

G3: not w in { w where w is Element of ExtREAL : ( 0 <= w & w < r ) } by XXREAL_1:def 2, G1, G2;

( 0 > w or w >= r ) by G3;

hence x in [.r,+infty.] by XXREAL_1:1, G2; :: thesis: verum

then x in { w where w is Element of ExtREAL : ( r <= w & w <= +infty ) } by XXREAL_1:def 1;

then consider w being Element of ExtREAL such that

H1: ( w = x & w >= r & w <= +infty ) ;

reconsider x = x as Element of ExtREAL by H1;

H2: x in [.0,+infty.] by A0, XXREAL_1:1, H1;

not x in [.0,r.[ by XXREAL_1:3, H1;

hence x in [.0,+infty.] \ [.0,r.[ by H2, XBOOLE_0:def 5; :: thesis: verum