let n be Element of NAT ; :: thesis: 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); :: thesis: ( 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) ; :: thesis: ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )

now :: thesis: ( ( 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) ; :: thesis: 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) ) ; :: thesis: verum

end;

case p in closed_inside_of_triangle (p1,p2,p3) ; :: thesis: 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 & 0 <= a2 & 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) ) ; :: thesis: verum

end;

end;

end;

hence ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ; :: thesis: verum