let a, b be Real; :: thesis: ( a <= b implies [.a,b.] = { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } )
set X = { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } ;
assume A1: a <= b ; :: thesis: [.a,b.] = { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) }

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } c= [.a,b.]

let x be object ; :: thesis: ( x in [.a,b.] implies b₁ in { (((1 - b₂) * a) + (b₂ * b)) where l is Real : ( 0 <= b₂ & b₂ <= 1 ) } )
assume A2: x in [.a,b.] ; :: thesis: b₁ in { (((1 - b₂) * a) + (b₂ * b)) where l is Real : ( 0 <= b₂ & b₂ <= 1 ) }
then reconsider y = x as Real ;
A3: ( a <= y & y <= b ) by A2, XXREAL_1:1;

per cases ( a < b or a = b ) by A1, XXREAL_0:1;

suppose a < b ; :: thesis: b₁ in { (((1 - b₂) * a) + (b₂ * b)) where l is Real : ( 0 <= b₂ & b₂ <= 1 ) }

then A4: b - a > b - b by XREAL_1:15;
reconsider l = (y - a) / (b - a) as Real ;
l in the carrier of (Closed-Interval-TSpace (0,1)) by A3, BORSUK_6:2;
then l in [.0,1.] by TOPMETR:18;
then A5: ( 0 <= l & l <= 1 ) by XXREAL_1:1;
((1 - l) * a) + (l * b) = a + (l * (b - a))
.= a + (y - a) by A4, XCMPLX_1:87
.= y ;
hence x in { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } by A5; :: thesis: verum

end;

suppose a = b ; :: thesis: b₁ in { (((1 - b₂) * a) + (b₂ * b)) where l is Real : ( 0 <= b₂ & b₂ <= 1 ) }

then ((1 - 1) * a) + (1 * b) = y by A3, XXREAL_0:1;
hence x in { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } ; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } or x in [.a,b.] )
assume x in { (((1 - l) * a) + (l * b)) where l is Real : ( 0 <= l & l <= 1 ) } ; :: thesis: x in [.a,b.]
then consider l being Real such that
A6: x = ((1 - l) * a) + (l * b) and
A7: ( 0 <= l & l <= 1 ) ;
( a <= ((1 - l) * a) + (l * b) & ((1 - l) * a) + (l * b) <= b ) by A1, A7, XREAL_1:172, XREAL_1:173;
hence x in [.a,b.] by A6, XXREAL_1:1; :: thesis: verum