let G be IncProjStr ; :: thesis: ( ex a, b, c being POINT of G st a,b,c is_a_triangle & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) implies ex p being POINT of G ex P being LINE of G st p |' P )

assume that

A1: ex a, b, c being POINT of G st a,b,c is_a_triangle and

A2: for p, q being POINT of G ex M being LINE of G st {p,q} on M ; :: thesis: ex p being POINT of G ex P being LINE of G st p |' P

consider a, b, c being POINT of G such that

A3: a,b,c is_a_triangle by A1;

consider P being LINE of G such that

A4: {a,b} on P by A2;

take c ; :: thesis: ex P being LINE of G st c |' P

take P ; :: thesis: c |' P

( a on P & b on P ) by A4, INCSP_1:1;

hence c |' P by A3, Th5; :: thesis: verum

assume that

A1: ex a, b, c being POINT of G st a,b,c is_a_triangle and

A2: for p, q being POINT of G ex M being LINE of G st {p,q} on M ; :: thesis: ex p being POINT of G ex P being LINE of G st p |' P

consider a, b, c being POINT of G such that

A3: a,b,c is_a_triangle by A1;

consider P being LINE of G such that

A4: {a,b} on P by A2;

take c ; :: thesis: ex P being LINE of G st c |' P

take P ; :: thesis: c |' P

( a on P & b on P ) by A4, INCSP_1:1;

hence c |' P by A3, Th5; :: thesis: verum