let AS be AffinSpace; :: thesis: 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

let A, K, M, N be Subset of AS; :: thesis: ( M is being_line & N is being_line & M,N,K is_coplanar & M,N,A is_coplanar & M <> N implies M,K,A is_coplanar )

assume that

A1: ( M is being_line & N is being_line ) and

A2: M,N,K is_coplanar and

A3: M,N,A is_coplanar and

A4: M <> N ; :: thesis: M,K,A is_coplanar

consider X being Subset of AS such that

A5: M c= X and

A6: N c= X and

A7: K c= X and

A8: X is being_plane by A2;

ex Y being Subset of AS st

( M c= Y & N c= Y & A c= Y & Y is being_plane ) by A3;

then A c= X by A1, A4, A5, A6, A8, Th26;

hence M,K,A is_coplanar by A5, A7, A8; :: thesis: verum

M,K,A is_coplanar

let A, K, M, N be Subset of AS; :: thesis: ( M is being_line & N is being_line & M,N,K is_coplanar & M,N,A is_coplanar & M <> N implies M,K,A is_coplanar )

assume that

A1: ( M is being_line & N is being_line ) and

A2: M,N,K is_coplanar and

A3: M,N,A is_coplanar and

A4: M <> N ; :: thesis: M,K,A is_coplanar

consider X being Subset of AS such that

A5: M c= X and

A6: N c= X and

A7: K c= X and

A8: X is being_plane by A2;

ex Y being Subset of AS st

( M c= Y & N c= Y & A c= Y & Y is being_plane ) by A3;

then A c= X by A1, A4, A5, A6, A8, Th26;

hence M,K,A is_coplanar by A5, A7, A8; :: thesis: verum