consider a, b, c, d being POINT of G such that
A1: a,b,c,d is_a_quadrangle by Th15;
reconsider e = [a,b,c,d] as Element of [: the Points of G, the Points of G, the Points of G, the Points of G:] ;
A2: e `3 = c by MCART_1:55;
take e ; :: thesis: e `1 ,e `2 ,e `3 ,e `4 is_a_quadrangle
( e `1 = a & e `2 = b ) by MCART_1:55;
hence e `1 ,e `2 ,e `3 ,e `4 is_a_quadrangle by A1, A2, MCART_1:55; :: thesis: verum