let AS be AffinSpace; 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; ( 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
; 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; verum