let AS be AffinSpace; :: thesis: for q being Element of AS
for K, M being Subset of AS 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 AS; :: thesis: for K, M being Subset of AS 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 AS; :: 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 AS 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 ) ; :: thesis: verum