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