let A be Subset of X; :: thesis: for v, w being Point of X st A = { (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 ) } holds
A = { (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 ) }
let v, w be Point of X; :: thesis: ( A = { (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 ) } implies A = { (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 ) } )
assume A1: A = { (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 ) } ; :: thesis: A = { (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 ) }
thus A c= { (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 ) } :: according to XBOOLE_0:def 10 :: thesis: { (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 ) } c= A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in { (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 ) } )
assume x in A ; :: thesis: x in { (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 ) }
then consider r being Real such that
A2: x = ((1 - r) * v) + (r * w) and
A3: ( 0 <= r & r <= 1 ) by A1;
A4: 1 - (1 - r) = r ;
( 0 <= 1 - r & 1 - r <= 1 - 0 ) by A3, XREAL_1:10, XREAL_1:48;
hence x in { (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 ) } by A2, A4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 ) } or x in A )
assume x in { (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 ) } ; :: thesis: x in A
then consider r being Real such that
A5: x = ((1 - r) * w) + (r * v) and
A6: ( 0 <= r & r <= 1 ) ;
A7: 1 - (1 - r) = r ;
( 0 <= 1 - r & 1 - r <= 1 - 0 ) by A6, XREAL_1:10, XREAL_1:48;
hence x in A by A1, A5, A7; :: thesis: verum