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