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