let PCPP be CollProjectiveSpace; :: thesis: for a1, a2, a3, c1, c3, x being Element of PCPP st not a1,a2,a3 are_collinear & a1,a2,c3 are_collinear & a2,a3,c1 are_collinear & c1,c3,x are_collinear & c3 <> a1 & c3 <> a2 & c1 <> a2 & c1 <> a3 holds
( a1 <> x & a3 <> x )
let a1, a2, a3, c1, c3, x be Element of PCPP; :: thesis: ( not a1,a2,a3 are_collinear & a1,a2,c3 are_collinear & a2,a3,c1 are_collinear & c1,c3,x are_collinear & c3 <> a1 & c3 <> a2 & c1 <> a2 & c1 <> a3 implies ( a1 <> x & a3 <> x ) )
assume that
A1: not a1,a2,a3 are_collinear and
A2: a1,a2,c3 are_collinear and
A3: a2,a3,c1 are_collinear and
A4: c1,c3,x are_collinear and
A5: c3 <> a1 and
A6: c3 <> a2 and
A7: c1 <> a2 and
A8: c1 <> a3 ; :: thesis: ( a1 <> x & a3 <> x )
A9: a3 <> x

proof

assume not a3 <> x ; :: thesis: contradiction
then A10: a3,c1,c3 are_collinear by A4, Th1;
a3,c1,a2 are_collinear by A3, Th1;
then a3,a2,c3 are_collinear by A8, A10, Th2;
then A11: a2,c3,a3 are_collinear by Th1;
a2,c3,a1 are_collinear by A2, Th1;
then a2,a1,a3 are_collinear by A6, A11, Th2;
hence contradiction by A1, Th1; :: thesis: verum

end;

a1 <> x

proof

assume not a1 <> x ; :: thesis: contradiction
then A12: a1,c3,c1 are_collinear by A4, Th1;
a1,c3,a2 are_collinear by A2, Th1;
then a1,c1,a2 are_collinear by A5, A12, Th2;
then A13: a2,c1,a1 are_collinear by Th1;
a2,c1,a3 are_collinear by A3, Th1;
then a2,a1,a3 are_collinear by A7, A13, Th2;
hence contradiction by A1, Th1; :: thesis: verum

end;

hence ( a1 <> x & a3 <> x ) by A9; :: thesis: verum