let G be IncProjStr ; :: thesis: ( G is IncProjSp implies ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle )

assume A1: G is IncProjSp ; :: thesis: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle

then consider A, B being LINE of G such that

A2: A <> B by Th7;

consider a, b being POINT of G such that

A3: ( a on A & a |' B ) and

A4: ( b on B & b |' A ) by A1, A2, PROJRED1:3;

consider q being POINT of G such that

A5: ( q on B & q |' A ) and

A6: b <> q by A1, A3, Th9;

A7: ( {b,q} on B & b,q |' A ) by A4, A5, INCSP_1:1;

A8: G is configuration by A1, Th4;

consider p being POINT of G such that

A9: ( p on A & p |' B ) and

A10: a <> p by A1, A3, Th9;

take a ; :: thesis: ex b, c, d being POINT of G st a,b,c,d is_a_quadrangle

take p ; :: thesis: ex c, d being POINT of G st a,p,c,d is_a_quadrangle

take b ; :: thesis: ex d being POINT of G st a,p,b,d is_a_quadrangle

take q ; :: thesis: a,p,b,q is_a_quadrangle

( {a,p} on A & a,p |' B ) by A3, A9, INCSP_1:1;

hence a,p,b,q is_a_quadrangle by A10, A6, A8, A7, Th14; :: thesis: verum

assume A1: G is IncProjSp ; :: thesis: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle

then consider A, B being LINE of G such that

A2: A <> B by Th7;

consider a, b being POINT of G such that

A3: ( a on A & a |' B ) and

A4: ( b on B & b |' A ) by A1, A2, PROJRED1:3;

consider q being POINT of G such that

A5: ( q on B & q |' A ) and

A6: b <> q by A1, A3, Th9;

A7: ( {b,q} on B & b,q |' A ) by A4, A5, INCSP_1:1;

A8: G is configuration by A1, Th4;

consider p being POINT of G such that

A9: ( p on A & p |' B ) and

A10: a <> p by A1, A3, Th9;

take a ; :: thesis: ex b, c, d being POINT of G st a,b,c,d is_a_quadrangle

take p ; :: thesis: ex c, d being POINT of G st a,p,c,d is_a_quadrangle

take b ; :: thesis: ex d being POINT of G st a,p,b,d is_a_quadrangle

take q ; :: thesis: a,p,b,q is_a_quadrangle

( {a,p} on A & a,p |' B ) by A3, A9, INCSP_1:1;

hence a,p,b,q is_a_quadrangle by A10, A6, A8, A7, Th14; :: thesis: verum