theorem Th12: :: BKMODEL2:20

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