theorem Th20: :: BKMODEL2:28

for P1, P2 being Element of absolute holds
( not pole_infty P1 = pole_infty P2 or P1 = P2 or ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 ) )