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 set ; :: 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

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, EUCLID:31
.= (((1 - lambda) * p1) + (lambda * p2)) + (0 * p3) by EUCLID:33 ;
A7: ((1 - lambda) + lambda) + 0 = 1 ;
1 - lambda >= 0 by A5, XREAL_1:50;
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, EUCLID:31
.= ((0 * p1) + ((1 - lambda) * p2)) + (lambda * p3) by EUCLID:33 ;
A12: (0 + (1 - lambda)) + lambda = 1 ;
1 - lambda >= 0 by A10, XREAL_1:50;
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, EUCLID:31
.= ((lambda * p1) + (0 * p2)) + ((1 - lambda) * p3) by EUCLID:33 ;
A17: (lambda + 0 ) + (1 - lambda) = 1 ;
1 - lambda >= 0 by A15, XREAL_1:50;
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