let a, b be real number ; :: 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 A1: a <= b ; :: thesis: [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b}
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 set ; :: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in {a,b} or x in [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) )
assume x in {a,b} ; :: thesis: x in [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b))
then A4: ( x = a or x = b ) by TARSKI:def 2;
A5: ( a in [.a,b.] & b in [.a,b.] ) by A1, XXREAL_1:1;
( a in left_closed_halfline a & b in right_closed_halfline b ) by XXREAL_1:234, XXREAL_1:236;
then ( a in (left_closed_halfline a) \/ (right_closed_halfline b) & b in (left_closed_halfline a) \/ (right_closed_halfline b) ) by XBOOLE_0:def 3;
hence x in [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) by A4, A5, XBOOLE_0:def 4; :: thesis: verum