for AS being AffinSpace
for A, K, M, N being Subset of AS st M is being_line & N is being_line & M,N,K is_coplanar & M,N,A is_coplanar & M <> N holds
M,K,A is_coplanar