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

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

P,Q,R are_mutually_distinct

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

P,Q,R are_mutually_distinct

let P, Q, R be LINE of G; :: thesis: ( a,b,c,d is_a_quadrangle & {a,b} on P & {a,c} on Q & {a,d} on R implies P,Q,R are_mutually_distinct )

assume that

A1: a,b,c,d is_a_quadrangle and

A2: {a,b} on P and

A3: {a,c} on Q and

A4: {a,d} on R ; :: thesis: P,Q,R are_mutually_distinct

c,d,a is_a_triangle by A1;

then a,c,d is_a_triangle by Th11;

then A5: Q <> R by A3, A4, Th19;

d,a,b is_a_triangle by A1;

then a,d,b is_a_triangle by Th11;

then A6: R <> P by A2, A4, Th19;

a,b,c is_a_triangle by A1;

then P <> Q by A2, A3, Th19;

hence P,Q,R are_mutually_distinct by A5, A6, ZFMISC_1:def 5; :: thesis: verum

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

P,Q,R are_mutually_distinct

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

P,Q,R are_mutually_distinct

let P, Q, R be LINE of G; :: thesis: ( a,b,c,d is_a_quadrangle & {a,b} on P & {a,c} on Q & {a,d} on R implies P,Q,R are_mutually_distinct )

assume that

A1: a,b,c,d is_a_quadrangle and

A2: {a,b} on P and

A3: {a,c} on Q and

A4: {a,d} on R ; :: thesis: P,Q,R are_mutually_distinct

c,d,a is_a_triangle by A1;

then a,c,d is_a_triangle by Th11;

then A5: Q <> R by A3, A4, Th19;

d,a,b is_a_triangle by A1;

then a,d,b is_a_triangle by Th11;

then A6: R <> P by A2, A4, Th19;

a,b,c is_a_triangle by A1;

then P <> Q by A2, A3, Th19;

hence P,Q,R are_mutually_distinct by A5, A6, ZFMISC_1:def 5; :: thesis: verum