theorem Th12: :: COMBGRAS:12

for k being Element of NAT
for X being non empty set st 0 < k & k + 1 c= card X holds
for A1, A2, A3, A4, A5, A6 being POINT of (G_ (k,X))
for L1, L2, L3, L4 being LINE of (G_ (k,X)) st A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 holds
ex A6 being POINT of (G_ (k,X)) st
( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )