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