let G be IncProjStr ; :: thesis: for a1, a2, b being POINT of G
for A being LINE of G st G is configuration & {a1,a2} on A & a1 <> a2 & b |' A holds
a1,a2,b is_a_triangle
let a1, a2, b be POINT of G; :: thesis: for A being LINE of G st G is configuration & {a1,a2} on A & a1 <> a2 & b |' A holds
a1,a2,b is_a_triangle
let A be LINE of G; :: thesis: ( G is configuration & {a1,a2} on A & a1 <> a2 & b |' A implies a1,a2,b is_a_triangle )
assume that
A1: G is configuration and
A2: {a1,a2} on A and
A3: ( a1 <> a2 & b |' A ) and
A4: a1,a2,b are_collinear ; :: thesis: contradiction
A5: ( a1 on A & a2 on A ) by A2, INCSP_1:1;
ex P being LINE of G st
( a1 on P & a2 on P & b on P ) by A4, Th5;
hence contradiction by A1, A3, A5; :: thesis: verum