theorem Th16: :: BKMODEL2:24

for P being Element of BK_model
for Q being Element of absolute ex R being Element of absolute st
( Q <> R & Q,P,R are_collinear )