let G be IncProjStr ; :: thesis: ( ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle implies ex a, b, c being POINT of G st a,b,c is_a_triangle )
given a, b, c, d being POINT of G such that A1: a,b,c,d is_a_quadrangle ; :: thesis: ex a, b, c being POINT of G st a,b,c is_a_triangle
take a ; :: thesis: ex b, c being POINT of G st a,b,c is_a_triangle
take b ; :: thesis: ex c being POINT of G st a,b,c is_a_triangle
take c ; :: thesis: a,b,c is_a_triangle
thus a,b,c is_a_triangle by A1, Def6; :: thesis: verum