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