theorem Th1: :: TRANSLAC:1

for AS being AffinSpace st ex a, b, c being Element of AS st
( LIN a,b,c & a <> b & a <> c & b <> c ) holds
for p, q being Element of AS ex r being Element of AS st
( LIN p,q,r & p <> r & q <> r )