theorem Th12: :: BKMODEL3:14

for P being Element of BK_model
for L being LINE of (IncProjSp_of real_projective_plane) st P in L holds
ex P1, P2 being Element of absolute st
( P1 <> P2 & P1 in L & P2 in L )