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 ( not a,b,c is_collinear & a,b // p,q & a,c // p,r & p <> q & p <> r ) ; :: thesis: not p,q,r is_collinear
then ( not a,b // a,c & a,b // p,q & a,c // p,r & p <> q & p <> r ) by Def2;
then not p,q // p,r by Th29;
hence not p,q,r is_collinear by Def2; :: thesis: verum