let SAS be Semi_Affine_Space; :: thesis: for a, b, c, p, q being Element of SAS st not a,b // a,c & p <> q & p,q // p,a & p,q // p,b holds
not p,q // p,c
let a, b, c, p, q be Element of SAS; :: thesis: ( not a,b // a,c & p <> q & p,q // p,a & p,q // p,b implies not p,q // p,c )
assume that
A1: not a,b // a,c and
A2: p <> q ; :: thesis: ( not p,q // p,a or not p,q // p,b or not p,q // p,c )

now :: thesis: ( a <> p & p,q // p,a & p,q // p,b implies not p,q // p,c )

assume that
A3: a <> p and
A4: p,q // p,a and
A5: p,q // p,b and
A6: p,q // p,c ; :: thesis: contradiction
p,a // p,c by A2, A4, A6, Def1;
then A7: a,p // a,c by Def1;
p,a // p,b by A2, A4, A5, Def1;
then a,p // a,b by Def1;
hence contradiction by A1, A3, A7, Def1; :: thesis: verum

end;

hence ( not p,q // p,a or not p,q // p,b or not p,q // p,c ) by A1, A2, Def1; :: thesis: verum