let p1, p2, p3, p be Point of (TOP-REAL 2); :: thesis:
assume A1: p2 - p1,p3 - p1 are_lindependent2 ; :: thesis:
A2: for p0 being Point of (TOP-REAL 2) holds
( p0 in Triangle p1,p2,p3 iff ( p0 in LSeg p1,p2 or p0 in LSeg p2,p3 or p0 in LSeg p3,p1 ) )

let p0 be Point of (TOP-REAL 2); :: thesis:
( p0 in Triangle p1,p2,p3 iff ( p0 in (LSeg p1,p2) \/ (LSeg p2,p3) or p0 in LSeg p3,p1 ) ) by XBOOLE_0:def 3;
hence ( p0 in Triangle p1,p2,p3 iff ( p0 in LSeg p1,p2 or p0 in LSeg p2,p3 or p0 in LSeg p3,p1 ) ) by XBOOLE_0:def 3; :: thesis:

end;

thus ( p in Triangle p1,p2,p3 implies ( 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 ) ) ) :: thesis:

set x = p;
assume A3: p in Triangle p1,p2,p3 ; :: thesis:

then consider lambda being Real such that
A5: p = ((1 - lambda) * p1) + (lambda * p2) and
A6: 0 <= lambda and
A7: lambda <= 1 ;
A8: p = (((1 - lambda) * p1) + (lambda * p2)) + (0. (TOP-REAL 2)) by A5, EUCLID:31
.= (((1 - lambda) * p1) + (lambda * p2)) + (0 * p3) by EUCLID:33 ;
A9: ((1 - lambda) + lambda) + 0 = 1 ;
1 - lambda >= 0 by A7, XREAL_1:50;
hence ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & ( a1 = 0 or a2 = 0 or a3 = 0 ) & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A6, A9, A8; :: thesis:

end;

then consider lambda being Real such that
A10: p = ((1 - lambda) * p2) + (lambda * p3) and
A11: 0 <= lambda and
A12: lambda <= 1 ;
A13: p = ((0. (TOP-REAL 2)) + ((1 - lambda) * p2)) + (lambda * p3) by A10, EUCLID:31
.= ((0 * p1) + ((1 - lambda) * p2)) + (lambda * p3) by EUCLID:33 ;
A14: (0 + (1 - lambda)) + lambda = 1 ;
1 - lambda >= 0 by A12, XREAL_1:50;
hence ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & ( a1 = 0 or a2 = 0 or a3 = 0 ) & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A11, A14, A13; :: thesis:

end;

then consider lambda being Real such that
A15: p = ((1 - lambda) * p3) + (lambda * p1) and
A16: 0 <= lambda and
A17: lambda <= 1 ;
A18: p = ((lambda * p1) + (0. (TOP-REAL 2))) + ((1 - lambda) * p3) by A15, EUCLID:31
.= ((lambda * p1) + (0 * p2)) + ((1 - lambda) * p3) by EUCLID:33 ;
A19: (lambda + 0 ) + (1 - lambda) = 1 ;
1 - lambda >= 0 by A17, XREAL_1:50;
hence ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & ( a1 = 0 or a2 = 0 or a3 = 0 ) & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A16, A19, A18; :: thesis:

end;

p in the carrier of (TOP-REAL 2) ;
then p in REAL 2 by EUCLID:25;
then p in plane p1,p2,p3 by A1, Th63;
hence ( 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 ) ) by A1, A4, Def11, Def12, Def13; :: thesis:

end;

thus ( 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 ) implies p in Triangle p1,p2,p3 ) :: thesis:

set p0 = p;
assume that
A20: tricord1 p1,p2,p3,p >= 0 and
A21: tricord2 p1,p2,p3,p >= 0 and
A22: tricord3 p1,p2,p3,p >= 0 and
A23: ( tricord1 p1,p2,p3,p = 0 or tricord2 p1,p2,p3,p = 0 or tricord3 p1,p2,p3,p = 0 ) ; :: thesis:
set i01 = tricord1 p1,p2,p3,p;
set i02 = tricord2 p1,p2,p3,p;
set i03 = tricord3 p1,p2,p3,p;
p in the carrier of (TOP-REAL 2) ;
then p in REAL 2 by EUCLID:25;
then A24: p in plane p1,p2,p3 by A1, Th63;

then consider a2, a3 being Real such that
A25: (0 + a2) + a3 = 1 and
A26: p = ((0 * p1) + (a2 * p2)) + (a3 * p3) by A1, A24, Def11;
a2 = tricord2 p1,p2,p3,p by A1, A24, A25, A26, Def12;
then A27: (1 - a3) + a3 >= 0 + a3 by A21, A25, XREAL_1:9;
A28: p = ((0. (TOP-REAL 2)) + (a2 * p2)) + (a3 * p3) by A26, EUCLID:33
.= (a2 * p2) + (a3 * p3) by EUCLID:31 ;
a3 = tricord3 p1,p2,p3,p by A1, A24, A25, A26, Def13;
hence ( p in LSeg p1,p2 or p in LSeg p2,p3 or p in LSeg p3,p1 ) by A22, A25, A28, A27; :: thesis:

end;

then consider a1, a3 being Real such that
A29: (a1 + 0 ) + a3 = 1 and
A30: p = ((a1 * p1) + (0 * p2)) + (a3 * p3) by A1, A24, Def12;
a1 = tricord1 p1,p2,p3,p by A1, A24, A29, A30, Def11;
then A31: (1 - a3) + a3 >= 0 + a3 by A20, A29, XREAL_1:9;
A32: p = ((a1 * p1) + (0. (TOP-REAL 2))) + (a3 * p3) by A30, EUCLID:33
.= (a1 * p1) + (a3 * p3) by EUCLID:31 ;
a3 = tricord3 p1,p2,p3,p by A1, A24, A29, A30, Def13;
then p in { (((1 - lambda) * p1) + (lambda * p3)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A22, A29, A32, A31;
hence ( p in LSeg p1,p2 or p in LSeg p2,p3 or p in LSeg p3,p1 ) by RLTOPSP1:def 2; :: thesis:

end;

then consider a1, a2 being Real such that
A33: (a1 + a2) + 0 = 1 and
A34: p = ((a1 * p1) + (a2 * p2)) + (0 * p3) by A1, A24, Def13;
a1 = tricord1 p1,p2,p3,p by A1, A24, A33, A34, Def11;
then A35: (1 - a2) + a2 >= 0 + a2 by A20, A33, XREAL_1:9;
A36: p = ((a1 * p1) + (a2 * p2)) + (0. (TOP-REAL 2)) by A34, EUCLID:33
.= (a1 * p1) + (a2 * p2) by EUCLID:31 ;
a2 = tricord2 p1,p2,p3,p by A1, A24, A33, A34, Def12;
hence ( p in LSeg p1,p2 or p in LSeg p2,p3 or p in LSeg p3,p1 ) by A21, A33, A36, A35; :: thesis:

end;

hence p in Triangle p1,p2,p3 by A2; :: thesis:

end;