let SAS be Semi_Affine_Space; :: thesis: for a, b, c, p, q, r being Element of SAS st not a,b,c is_collinear & a,b // p,q & a,c // p,r & p <> q & p <> r holds
not p,q,r is_collinear
let a, b, c, p, q, r be Element of SAS; :: thesis: ( not a,b,c is_collinear & a,b // p,q & a,c // p,r & p <> q & p <> r implies not p,q,r is_collinear )
assume that
A1: not a,b,c is_collinear and
A2: ( a,b // p,q & a,c // p,r & p <> q & p <> r ) ; :: thesis: not p,q,r is_collinear
not a,b // a,c by A1, Def2;
then not p,q // p,r by A2, Th29;
hence not p,q,r is_collinear by Def2; :: thesis: verum