for AS being AffinSpace
for K, M, N being Subset of AS st K,M,N is_coplanar holds
( K,N,M is_coplanar & M,K,N is_coplanar & M,N,K is_coplanar & N,K,M is_coplanar & N,M,K is_coplanar ) ;