let PCPP be CollProjectiveSpace; :: thesis: for a, b, c, d being Element of PCPP st not a,b,c are_collinear & a,b,d are_collinear & a,c,d are_collinear holds
a = d
let a, b, c, d be Element of PCPP; :: thesis: ( not a,b,c are_collinear & a,b,d are_collinear & a,c,d are_collinear implies a = d )
assume that
A1: not a,b,c are_collinear and
A2: ( a,b,d are_collinear & a,c,d are_collinear ) ; :: thesis: a = d
assume A3: not a = d ; :: thesis: contradiction
A4: a,d,a are_collinear by ANPROJ_2:def 7;
( a,d,b are_collinear & a,d,c are_collinear ) by A2, Th1;
hence contradiction by A1, A3, A4, ANPROJ_2:def 8; :: thesis: verum