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