let SAS be Semi_Affine_Space; :: thesis: for a, b, c, p, q, r1, r2 being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c // q,r1 & b,c // q,r2 holds
r1 = r2
let a, b, c, p, q, r1, r2 be Element of SAS; :: thesis: ( not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c // q,r1 & b,c // q,r2 implies r1 = r2 )
assume A1: ( not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c // q,r1 & b,c // q,r2 ) ; :: thesis: r1 = r2

A2: now

assume p = q ; :: thesis: r1 = r2
then ( p = r1 & p = r2 ) by A1, Th31;
hence r1 = r2 ; :: thesis: verum

end;

now

assume p <> q ; :: thesis: r1 = r2
then ( not p,q // p,r1 & a <> c & b <> c & a,c // p,r1 & a,c // p,r2 & b,c // q,r1 & b,c // q,r2 ) by A1, Def1, Th12, Th30;
then ( not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 ) by Def1;
hence r1 = r2 by Th32; :: thesis: verum

end;

hence r1 = r2 by A2; :: thesis: verum