let a, b be Real; ( a <= b implies [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b} )
set A = left_closed_halfline a;
set B = right_closed_halfline b;
assume
a <= b
; [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b}
then A1:
( a in [.a,b.] & b in [.a,b.] )
by XXREAL_1:1;
thus
[.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) c= {a,b}
XBOOLE_0:def 10 {a,b} c= [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b))proof
let x be
object ;
TARSKI:def 3 ( not x in [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) or x in {a,b} )
assume A2:
x in [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b))
;
x in {a,b}
then reconsider x =
x as
Real ;
x in (left_closed_halfline a) \/ (right_closed_halfline b)
by A2, XBOOLE_0:def 4;
then
(
x in left_closed_halfline a or
x in right_closed_halfline b )
by XBOOLE_0:def 3;
then A3:
(
x <= a or
x >= b )
by XXREAL_1:234, XXREAL_1:236;
x in [.a,b.]
by A2, XBOOLE_0:def 4;
then
(
a <= x &
x <= b )
by XXREAL_1:1;
then
(
x = a or
x = b )
by A3, XXREAL_0:1;
hence
x in {a,b}
by TARSKI:def 2;
verum
end;
let x be object ; TARSKI:def 3 ( not x in {a,b} or x in [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) )
a in left_closed_halfline a
by XXREAL_1:234;
then A4:
a in (left_closed_halfline a) \/ (right_closed_halfline b)
by XBOOLE_0:def 3;
b in right_closed_halfline b
by XXREAL_1:236;
then A5:
b in (left_closed_halfline a) \/ (right_closed_halfline b)
by XBOOLE_0:def 3;
assume
x in {a,b}
; x in [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b))
then
( x = a or x = b )
by TARSKI:def 2;
hence
x in [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b))
by A1, A4, A5, XBOOLE_0:def 4; verum