theorem Th14:
for
PCPP being
CollProjectiveSpace for
a1,
a2,
b1,
b2,
x,
y being
Element of
PCPP st
a1 <> a2 &
b1 <> b2 &
b1,
b2,
x are_collinear &
b1,
b2,
y are_collinear &
a1,
a2,
x are_collinear &
a1,
a2,
y are_collinear & not
a1,
a2,
b1 are_collinear holds
x = y