let n be Element of NAT ; :: thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds Triangle (p1,p2,p3) c= closed_inside_of_triangle (p1,p2,p3)
let p1, p2, p3 be Point of (TOP-REAL n); :: thesis: Triangle (p1,p2,p3) c= closed_inside_of_triangle (p1,p2,p3)
((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1)) c= closed_inside_of_triangle (p1,p2,p3)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1)) or x in closed_inside_of_triangle (p1,p2,p3) )
assume A1: x in ((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1)) ; :: thesis: x in closed_inside_of_triangle (p1,p2,p3)
then reconsider p0 = x as Point of (TOP-REAL n) ;
A2: ( x in (LSeg (p1,p2)) \/ (LSeg (p2,p3)) or x in LSeg (p3,p1) ) by A1, XBOOLE_0:def 3;

now :: thesis: ( ( x in LSeg (p1,p2) & ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) or ( x in LSeg (p2,p3) & ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) or ( x in LSeg (p3,p1) & ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) )

per cases ( x in LSeg (p1,p2) or x in LSeg (p2,p3) or x in LSeg (p3,p1) ) by A2, XBOOLE_0:def 3;

case x in LSeg (p1,p2) ; :: thesis: ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )

then consider lambda being Real such that
A3: x = ((1 - lambda) * p1) + (lambda * p2) and
A4: 0 <= lambda and
A5: lambda <= 1 ;
A6: p0 = (((1 - lambda) * p1) + (lambda * p2)) + (0. (TOP-REAL n)) by A3, RLVECT_1:4
.= (((1 - lambda) * p1) + (lambda * p2)) + (0 * p3) by RLVECT_1:10 ;
A7: ((1 - lambda) + lambda) + 0 = 1 ;
1 - lambda >= 0 by A5, XREAL_1:48;
hence ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A4, A7, A6; :: thesis: verum

end;

case x in LSeg (p2,p3) ; :: thesis: ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )

then consider lambda being Real such that
A8: x = ((1 - lambda) * p2) + (lambda * p3) and
A9: 0 <= lambda and
A10: lambda <= 1 ;
A11: p0 = ((0. (TOP-REAL n)) + ((1 - lambda) * p2)) + (lambda * p3) by A8, RLVECT_1:4
.= ((0 * p1) + ((1 - lambda) * p2)) + (lambda * p3) by RLVECT_1:10 ;
A12: (0 + (1 - lambda)) + lambda = 1 ;
1 - lambda >= 0 by A10, XREAL_1:48;
hence ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A9, A12, A11; :: thesis: verum

end;

case x in LSeg (p3,p1) ; :: thesis: ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )

then consider lambda being Real such that
A13: x = ((1 - lambda) * p3) + (lambda * p1) and
A14: 0 <= lambda and
A15: lambda <= 1 ;
A16: p0 = ((lambda * p1) + (0. (TOP-REAL n))) + ((1 - lambda) * p3) by A13, RLVECT_1:4
.= ((lambda * p1) + (0 * p2)) + ((1 - lambda) * p3) by RLVECT_1:10 ;
A17: (lambda + 0) + (1 - lambda) = 1 ;
1 - lambda >= 0 by A15, XREAL_1:48;
hence ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A14, A17, A16; :: thesis: verum

end;

end;

end;

hence x in closed_inside_of_triangle (p1,p2,p3) ; :: thesis: verum

end;

hence Triangle (p1,p2,p3) c= closed_inside_of_triangle (p1,p2,p3) ; :: thesis: verum