let n be Element of NAT ; for p1, p2, p3, p being Point of (TOP-REAL n) st p in plane (p1,p2,p3) holds
ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
let p1, p2, p3, p be Point of (TOP-REAL n); ( p in plane (p1,p2,p3) implies ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) )
assume A1:
p in plane (p1,p2,p3)
; ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
now ( ( p in outside_of_triangle (p1,p2,p3) & ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) or ( p in closed_inside_of_triangle (p1,p2,p3) & ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) )per cases
( p in outside_of_triangle (p1,p2,p3) or p in closed_inside_of_triangle (p1,p2,p3) )
by A1, XBOOLE_0:def 3;
case
p in outside_of_triangle (
p1,
p2,
p3)
;
ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )then
ex
p4 being
Point of
(TOP-REAL n) st
(
p4 = p & ex
a1,
a2,
a3 being
Real st
( (
0 > a1 or
0 > a2 or
0 > a3 ) &
(a1 + a2) + a3 = 1 &
p4 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) )
;
hence
ex
a1,
a2,
a3 being
Real st
(
(a1 + a2) + a3 = 1 &
p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
;
verum end; end; end;
hence
ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
; verum