let n be Element of NAT ; :: thesis: for r being real number
for y, z being Point of (TOP-REAL n)
for x being set st x = ((1 - r) * y) + (r * z) holds
( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) )
let r be real number ; :: thesis: for y, z being Point of (TOP-REAL n)
for x being set st x = ((1 - r) * y) + (r * z) holds
( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) )
let y, z be Point of (TOP-REAL n); :: thesis: for x being set st x = ((1 - r) * y) + (r * z) holds
( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) )
let x be set ; :: thesis: ( x = ((1 - r) * y) + (r * z) implies ( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) ) )
assume A1: x = ((1 - r) * y) + (r * z) ; :: thesis: ( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) )
hereby :: thesis: ( ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) )
assume x = y ; :: thesis: ( r = 0 or y = z )
then 0. (TOP-REAL n) = (((1 - r) * y) + (r * z)) - y by A1, EUCLID:46
.= (((1 - r) * y) - y) + (r * z) by JORDAN2C:9
.= (((1 - r) * y) - (1 * y)) + (r * z) by EUCLID:33
.= (((1 - r) - 1) * y) + (r * z) by EUCLID:54
.= ((- r) * y) + (r * z)
.= (r * z) - (r * y) by EUCLID:44
.= r * (z - y) by EUCLID:53 ;
then ( r = 0 or z - y = 0. (TOP-REAL n) ) by EUCLID:35;
hence ( r = 0 or y = z ) by EUCLID:47; :: thesis: verum
end;
hereby :: thesis: ( x = z iff ( r = 1 or y = z ) )
assume A2: ( r = 0 or y = z ) ; :: thesis: x = y
per cases ( r = 0 or z = y ) by A2;
suppose r = 0 ; :: thesis: x = y
hence x = y + (0 * z) by A1, EUCLID:33
.= y + (0. (TOP-REAL n)) by EUCLID:33
.= y by EUCLID:31 ;
:: thesis: verum
end;
suppose z = y ; :: thesis: x = y
hence x = ((1 - r) + r) * y by A1, EUCLID:37
.= y by EUCLID:33 ;
:: thesis: verum
end;
end;
end;
hereby :: thesis: ( ( r = 1 or y = z ) implies x = z )
assume x = z ; :: thesis: ( r = 1 or y = z )
then 0. (TOP-REAL n) = (((1 - r) * y) + (r * z)) - z by A1, EUCLID:46
.= ((1 - r) * y) + ((r * z) - z) by EUCLID:49
.= ((1 - r) * y) + ((r * z) + ((- 1) * z)) by EUCLID:43
.= ((1 - r) * y) + (((- 1) + r) * z) by EUCLID:37
.= ((1 - r) * y) + ((- (1 - r)) * z)
.= ((1 - r) * y) - ((1 - r) * z) by EUCLID:44
.= (1 - r) * (y - z) by EUCLID:53 ;
then ( (1 - r) + r = 0 + r or y - z = 0. (TOP-REAL n) ) by EUCLID:35;
hence ( r = 1 or y = z ) by EUCLID:47; :: thesis: verum
end;
assume A3: ( r = 1 or y = z ) ; :: thesis: x = z
per cases ( r = 1 or y = z ) by A3;
suppose r = 1 ; :: thesis: x = z
hence x = (0. (TOP-REAL n)) + (1 * z) by A1, EUCLID:33
.= 1 * z by EUCLID:31
.= z by EUCLID:33 ;
:: thesis: verum
end;
suppose y = z ; :: thesis: x = z
hence x = ((1 - r) + r) * z by A1, EUCLID:37
.= z by EUCLID:33 ;
:: thesis: verum
end;
end;