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

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