let AS be AffinSpace; :: thesis: for K, M, N being Subset of AS st K,M,N is_coplanar holds
( K,N,M is_coplanar & M,K,N is_coplanar & M,N,K is_coplanar & N,K,M is_coplanar & N,M,K is_coplanar )
let K, M, N be Subset of AS; :: thesis: ( K,M,N is_coplanar implies ( K,N,M is_coplanar & M,K,N is_coplanar & M,N,K is_coplanar & N,K,M is_coplanar & N,M,K is_coplanar ) )
assume K,M,N is_coplanar ; :: thesis: ( K,N,M is_coplanar & M,K,N is_coplanar & M,N,K is_coplanar & N,K,M is_coplanar & N,M,K is_coplanar )
then ex X being Subset of AS st
( K c= X & M c= X & N c= X & X is being_plane ) by Def5;
hence ( K,N,M is_coplanar & M,K,N is_coplanar & M,N,K is_coplanar & N,K,M is_coplanar & N,M,K is_coplanar ) by Def5; :: thesis: verum