for AS being AffinSpace
for A, K, M, X being Subset of AS st K is being_line & M is being_line & X is being_plane & K c= X & M c= X & K <> M holds
( K,M,A is_coplanar iff A c= X ) by Th26;