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:59;
take e ; :: thesis: e `1 ,e `2 ,e `3 ,e `4 is_a_quadrangle
( e `1 = a & e `2 = b ) by MCART_1:59;
hence e `1 ,e `2 ,e `3 ,e `4 is_a_quadrangle by A1, A2, MCART_1:59; :: thesis: verum