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_4 = c by MCART_1:def 10;

take e ; :: thesis: e `1_4 ,e `2_4 ,e `3_4 ,e `4_4 is_a_quadrangle

( e `1_4 = a & e `2_4 = b ) by MCART_1:def 8, MCART_1:def 9;

hence e `1_4 ,e `2_4 ,e `3_4 ,e `4_4 is_a_quadrangle by A1, A2, MCART_1:def 11; :: thesis: verum

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_4 = c by MCART_1:def 10;

take e ; :: thesis: e `1_4 ,e `2_4 ,e `3_4 ,e `4_4 is_a_quadrangle

( e `1_4 = a & e `2_4 = b ) by MCART_1:def 8, MCART_1:def 9;

hence e `1_4 ,e `2_4 ,e `3_4 ,e `4_4 is_a_quadrangle by A1, A2, MCART_1:def 11; :: thesis: verum