let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d, x being Element of SAS st not a,b,c is_collinear & a,b // c,d & c <> d & c,d,x is_collinear holds
not a,b,x is_collinear
let a, b, c, d, x be Element of SAS; :: thesis: ( not a,b,c is_collinear & a,b // c,d & c <> d & c,d,x is_collinear implies not a,b,x is_collinear )
assume A1: ( not a,b,c is_collinear & a,b // c,d & c <> d & c,d,x is_collinear ) ; :: thesis: not a,b,x is_collinear
then ( c <> d & a,b // c,d & c,d // c,x ) by Def2;
hence not a,b,x is_collinear by A1, Th20, Th43; :: thesis: verum