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

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