let n be Element of NAT ; 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); 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 ;
TARSKI:def 3 ( 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))
;
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 ( ( 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) ) ) )end;
hence
x in closed_inside_of_triangle (
p1,
p2,
p3)
;
verum
end;
hence
Triangle (p1,p2,p3) c= closed_inside_of_triangle (p1,p2,p3)
; verum