let a, b, c be real number ; :: thesis: ( a <= c & c <= b implies [.a,b.] \/ [.c,+infty .[ = [.a,+infty .[ )
assume A1: ( a <= c & c <= b ) ; :: thesis: [.a,b.] \/ [.c,+infty .[ = [.a,+infty .[
A2: [.a,+infty .[ c= [.a,b.] \/ [.c,+infty .[

proof

let r be set ; :: according to TARSKI:def 3 :: thesis: ( not r in [.a,+infty .[ or r in [.a,b.] \/ [.c,+infty .[ )
assume A3: r in [.a,+infty .[ ; :: thesis: r in [.a,b.] \/ [.c,+infty .[
then reconsider s = r as Real ;
A4: a <= s by A3, XXREAL_1:236;

per cases ( s <= b or not s <= b ) ;

suppose s <= b ; :: thesis: r in [.a,b.] \/ [.c,+infty .[

then s in [.a,b.] by A4, XXREAL_1:1;
hence r in [.a,b.] \/ [.c,+infty .[ by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not s <= b ; :: thesis: r in [.a,b.] \/ [.c,+infty .[

then c <= s by A1, XXREAL_0:2;
then s in [.c,+infty .[ by XXREAL_1:236;
hence r in [.a,b.] \/ [.c,+infty .[ by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

[.a,b.] \/ [.c,+infty .[ c= [.a,+infty .[

proof

A5: [.a,b.] c= right_closed_halfline a by XXREAL_1:251;
[.c,+infty .[ c= [.a,+infty .[ by A1, XXREAL_1:38;
hence [.a,b.] \/ [.c,+infty .[ c= [.a,+infty .[ by A5, XBOOLE_1:8; :: thesis: verum

end;

hence [.a,b.] \/ [.c,+infty .[ = [.a,+infty .[ by A2, XBOOLE_0:def 10; :: thesis: verum