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 x in { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } ;
then consider lambda being Real such that
A3: ( x = ((1 - lambda) * p1) + (lambda * p2) & 0 <= lambda & lambda <= 1 ) ;
A4: 1 - lambda >= 0 by A3, XREAL_1:50;
A5: ((1 - lambda) + lambda) + 0 = 1 ;
p0 = (((1 - lambda) * p1) + (lambda * p2)) + (0. (TOP-REAL n)) by A3, EUCLID:31
.= (((1 - lambda) * p1) + (lambda * p2)) + (0 * p3) by EUCLID:33 ;
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 A3, A4, A5; :: 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 x in { (((1 - lambda) * p2) + (lambda * p3)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } ;
then consider lambda being Real such that
A6: ( x = ((1 - lambda) * p2) + (lambda * p3) & 0 <= lambda & lambda <= 1 ) ;
A7: 1 - lambda >= 0 by A6, XREAL_1:50;
A8: (0 + (1 - lambda)) + lambda = 1 ;
p0 = ((0. (TOP-REAL n)) + ((1 - lambda) * p2)) + (lambda * p3) by A6, EUCLID:31
.= ((0 * p1) + ((1 - lambda) * p2)) + (lambda * p3) by EUCLID:33 ;
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 A6, A7, A8; :: 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 x in { (((1 - lambda) * p3) + (lambda * p1)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } ;
then consider lambda being Real such that
A9: ( x = ((1 - lambda) * p3) + (lambda * p1) & 0 <= lambda & lambda <= 1 ) ;
A10: 1 - lambda >= 0 by A9, XREAL_1:50;
A11: (lambda + 0 ) + (1 - lambda) = 1 ;
p0 = ((lambda * p1) + (0. (TOP-REAL n))) + ((1 - lambda) * p3) by A9, EUCLID:31
.= ((lambda * p1) + (0 * p2)) + ((1 - lambda) * p3) by EUCLID:33 ;
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, A10, A11; :: 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