theorem Th56:
for
p1,
p2,
p3,
p being
Point of
(TOP-REAL 2) st
p2 - p1,
p3 - p1 are_lindependent2 holds
(
p in Triangle (
p1,
p2,
p3) iff (
tricord1 (
p1,
p2,
p3,
p)
>= 0 &
tricord2 (
p1,
p2,
p3,
p)
>= 0 &
tricord3 (
p1,
p2,
p3,
p)
>= 0 & (
tricord1 (
p1,
p2,
p3,
p)
= 0 or
tricord2 (
p1,
p2,
p3,
p)
= 0 or
tricord3 (
p1,
p2,
p3,
p)
= 0 ) ) )