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.] )
proof
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.[ )
proof
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;
assume x in [.r,+infty.] ; :: thesis: 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;
hence [.0,+infty.] \ [.0,r.[ = [.r,+infty.] ; :: thesis: verum