:: deftheorem defines is_coplanar AFF_4:def 5 :
for AS being AffinSpace
for K, M, N being Subset of AS holds
( K,M,N is_coplanar iff ex X being Subset of AS st
( K c= X & M c= X & N c= X & X is being_plane ) );