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 A1: ( not a,b // a,c & p <> q ) ; :: thesis: ( not p,q // p,a or not p,q // p,b or not p,q // p,c )

now

assume ( a <> p & p,q // p,a & p,q // p,b & p,q // p,c ) ; :: thesis: contradiction
then ( a <> p & p,a // p,b & p,a // p,c ) by A1, Def1;
then ( a <> p & a,p // a,b & a,p // a,c ) by Def1;
hence contradiction by A1, Def1; :: thesis: verum

end;

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