let G be IncProjStr ; :: thesis: for a, b, c being POINT of G

for P, Q being LINE of G st a,b,c is_a_triangle & {a,b} on P & {a,c} on Q holds

P <> Q

let a, b, c be POINT of G; :: thesis: for P, Q being LINE of G st a,b,c is_a_triangle & {a,b} on P & {a,c} on Q holds

P <> Q

let P, Q be LINE of G; :: thesis: ( a,b,c is_a_triangle & {a,b} on P & {a,c} on Q implies P <> Q )

assume that

A1: a,b,c is_a_triangle and

A2: {a,b} on P and

A3: {a,c} on Q ; :: thesis: P <> Q

A4: c on Q by A3, INCSP_1:1;

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

hence P <> Q by A1, A4, Th5; :: thesis: verum

for P, Q being LINE of G st a,b,c is_a_triangle & {a,b} on P & {a,c} on Q holds

P <> Q

let a, b, c be POINT of G; :: thesis: for P, Q being LINE of G st a,b,c is_a_triangle & {a,b} on P & {a,c} on Q holds

P <> Q

let P, Q be LINE of G; :: thesis: ( a,b,c is_a_triangle & {a,b} on P & {a,c} on Q implies P <> Q )

assume that

A1: a,b,c is_a_triangle and

A2: {a,b} on P and

A3: {a,c} on Q ; :: thesis: P <> Q

A4: c on Q by A3, INCSP_1:1;

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

hence P <> Q by A1, A4, Th5; :: thesis: verum