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 that
A1: ( not a,b,c is_collinear & a,b // c,d & c <> d ) and
A2: c,d,x is_collinear ; :: thesis: not a,b,x is_collinear
c,d // c,x by A2, Def2;
hence not a,b,x is_collinear by A1, Th20, Th43; :: thesis: verum