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
; 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; verum