let S be Subset of V; for v, w being Point of V st S = { (((1 - r) * v) + (r * w)) where r is Real : verum } holds
S = { (((1 - r) * w) + (r * v)) where r is Real : verum }
let v, w be Point of V; ( S = { (((1 - r) * v) + (r * w)) where r is Real : verum } implies S = { (((1 - r) * w) + (r * v)) where r is Real : verum } )
set A = { (((1 - r) * w) + (r * v)) where r is Real : verum } ;
assume A1:
S = { (((1 - r) * v) + (r * w)) where r is Real : verum }
; S = { (((1 - r) * w) + (r * v)) where r is Real : verum }
thus
S c= { (((1 - r) * w) + (r * v)) where r is Real : verum }
XBOOLE_0:def 10 { (((1 - r) * w) + (r * v)) where r is Real : verum } c= Sproof
let e be
object ;
TARSKI:def 3 ( not e in S or e in { (((1 - r) * w) + (r * v)) where r is Real : verum } )
assume
e in S
;
e in { (((1 - r) * w) + (r * v)) where r is Real : verum }
then consider r being
Real such that A2:
e = ((1 - r) * v) + (r * w)
by A1;
e = ((1 - (1 - r)) * w) + ((1 - r) * v)
by A2;
hence
e in { (((1 - r) * w) + (r * v)) where r is Real : verum }
;
verum
end;
let e be object ; TARSKI:def 3 ( not e in { (((1 - r) * w) + (r * v)) where r is Real : verum } or e in S )
assume
e in { (((1 - r) * w) + (r * v)) where r is Real : verum }
; e in S
then consider r being Real such that
A3:
e = ((1 - r) * w) + (r * v)
;
e = ((1 - (1 - r)) * v) + ((1 - r) * w)
by A3;
hence
e in S
by A1; verum