let G be IncProjStr ; :: thesis: for a1, a2, b1, b2 being POINT of G

for A, B being LINE of G st G is configuration & {a1,a2} on A & {b1,b2} on B & a1,a2 |' B & b1,b2 |' A & a1 <> a2 & b1 <> b2 holds

a1,a2,b1,b2 is_a_quadrangle

let a1, a2, b1, b2 be POINT of G; :: thesis: for A, B being LINE of G st G is configuration & {a1,a2} on A & {b1,b2} on B & a1,a2 |' B & b1,b2 |' A & a1 <> a2 & b1 <> b2 holds

a1,a2,b1,b2 is_a_quadrangle

let A, B be LINE of G; :: thesis: ( G is configuration & {a1,a2} on A & {b1,b2} on B & a1,a2 |' B & b1,b2 |' A & a1 <> a2 & b1 <> b2 implies a1,a2,b1,b2 is_a_quadrangle )

assume that

A1: G is configuration and

A2: {a1,a2} on A and

A3: {b1,b2} on B and

A4: a1,a2 |' B and

A5: b1,b2 |' A and

A6: a1 <> a2 and

A7: b1 <> b2 ; :: thesis: a1,a2,b1,b2 is_a_quadrangle

b1 |' A by A5;

then A8: a1,a2,b1 is_a_triangle by A1, A2, A6, Th10;

b2 |' A by A5;

then a1,a2,b2 is_a_triangle by A1, A2, A6, Th10;

then A9: b2,a1,a2 is_a_triangle by Th11;

a2 |' B by A4;

then b1,b2,a2 is_a_triangle by A1, A3, A7, Th10;

then A10: a2,b1,b2 is_a_triangle by Th11;

a1 |' B by A4;

then b1,b2,a1 is_a_triangle by A1, A3, A7, Th10;

hence a1,a2,b1,b2 is_a_quadrangle by A8, A10, A9; :: thesis: verum

for A, B being LINE of G st G is configuration & {a1,a2} on A & {b1,b2} on B & a1,a2 |' B & b1,b2 |' A & a1 <> a2 & b1 <> b2 holds

a1,a2,b1,b2 is_a_quadrangle

let a1, a2, b1, b2 be POINT of G; :: thesis: for A, B being LINE of G st G is configuration & {a1,a2} on A & {b1,b2} on B & a1,a2 |' B & b1,b2 |' A & a1 <> a2 & b1 <> b2 holds

a1,a2,b1,b2 is_a_quadrangle

let A, B be LINE of G; :: thesis: ( G is configuration & {a1,a2} on A & {b1,b2} on B & a1,a2 |' B & b1,b2 |' A & a1 <> a2 & b1 <> b2 implies a1,a2,b1,b2 is_a_quadrangle )

assume that

A1: G is configuration and

A2: {a1,a2} on A and

A3: {b1,b2} on B and

A4: a1,a2 |' B and

A5: b1,b2 |' A and

A6: a1 <> a2 and

A7: b1 <> b2 ; :: thesis: a1,a2,b1,b2 is_a_quadrangle

b1 |' A by A5;

then A8: a1,a2,b1 is_a_triangle by A1, A2, A6, Th10;

b2 |' A by A5;

then a1,a2,b2 is_a_triangle by A1, A2, A6, Th10;

then A9: b2,a1,a2 is_a_triangle by Th11;

a2 |' B by A4;

then b1,b2,a2 is_a_triangle by A1, A3, A7, Th10;

then A10: a2,b1,b2 is_a_triangle by Th11;

a1 |' B by A4;

then b1,b2,a1 is_a_triangle by A1, A3, A7, Th10;

hence a1,a2,b1,b2 is_a_quadrangle by A8, A10, A9; :: thesis: verum