let AS be AffinSpace; :: thesis: for K, M, X, A 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 )
let K, M, X, A be Subset of AS; :: thesis: ( K is being_line & M is being_line & X is being_plane & K c= X & M c= X & K <> M implies ( K,M,A is_coplanar iff A c= X ) )
assume that
A1: ( K is being_line & M is being_line ) and
A2: ( X is being_plane & K c= X & M c= X ) and
A3: K <> M ; :: thesis: ( K,M,A is_coplanar iff A c= X )

now

assume K,M,A is_coplanar ; :: thesis: A c= X
then ex Y being Subset of AS st
( K c= Y & M c= Y & A c= Y & Y is being_plane ) by Def5;
hence A c= X by A1, A2, A3, Th26; :: thesis: verum

end;

hence ( K,M,A is_coplanar iff A c= X ) by A2, Def5; :: thesis: verum