let a, b, c be Real; :: thesis: ( a <= c & c <= b implies [.a,b.] \/ [.c,+infty.[ = [.a,+infty.[ )
assume that
A1: a <= c and
A2: c <= b ; :: thesis: [.a,b.] \/ [.c,+infty.[ = [.a,+infty.[
A3: [.a,+infty.[ c= [.a,b.] \/ [.c,+infty.[
proof
let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in [.a,+infty.[ or r in [.a,b.] \/ [.c,+infty.[ )
assume A4: r in [.a,+infty.[ ; :: thesis: r in [.a,b.] \/ [.c,+infty.[
then reconsider s = r as Real ;
A5: a <= s by A4, XXREAL_1:236;
per cases ( s <= b or not s <= b ) ;
end;
end;
A6: [.a,b.] c= right_closed_halfline a by XXREAL_1:251;
[.c,+infty.[ c= [.a,+infty.[ by A1, XXREAL_1:38;
then [.a,b.] \/ [.c,+infty.[ c= [.a,+infty.[ by A6, XBOOLE_1:8;
hence [.a,b.] \/ [.c,+infty.[ = [.a,+infty.[ by A3, XBOOLE_0:def 10; :: thesis: verum