let PCPP be CollProjectiveSpace; :: thesis: 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
let a1, a2, b1, b2, x, y be Element of PCPP; :: thesis: ( 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 implies x = y )
assume that
A1: a1 <> a2 and
A2: ( b1 <> b2 & b1,b2,x are_collinear & b1,b2,y are_collinear ) and
A3: ( a1,a2,x are_collinear & a1,a2,y are_collinear ) and
A4: not a1,a2,b1 are_collinear ; :: thesis: x = y
a1,a2,a2 are_collinear by ANPROJ_2:def 7;
then A5: x,y,a2 are_collinear by A1, A3, ANPROJ_2:def 8;
b1,b2,b1 are_collinear by ANPROJ_2:def 7;
then A6: x,y,b1 are_collinear by A2, ANPROJ_2:def 8;
assume A7: not x = y ; :: thesis: contradiction
a1,a2,a1 are_collinear by ANPROJ_2:def 7;
then x,y,a1 are_collinear by A1, A3, ANPROJ_2:def 8;
hence contradiction by A4, A7, A6, A5, ANPROJ_2:def 8; :: thesis: verum