let a, b be Real; :: thesis: ( 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 ; :: thesis: [.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} :: according to XBOOLE_0:def 10 :: thesis: {a,b} c= [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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)) ; :: thesis: 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; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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} ; :: thesis: 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; :: thesis: verum