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 that
A1: not a,b // a,c and
A2: a,b // p,q and
A3: a,c // p,r1 and
A4: a,c // p,r2 and
A5: b,c // q,r1 and
A6: b,c // q,r2 ; :: thesis: r1 = r2
A7: now :: thesis: ( p <> q implies r1 = r2 )
b <> c by A1, Th1;
then A8: q,r1 // q,r2 by A5, A6, Def1;
a <> c by A1, Def1;
then A9: p,r1 // p,r2 by A3, A4, Def1;
assume p <> q ; :: thesis: r1 = r2
then not p,q // p,r1 by A1, A2, A3, A5, Th16;
hence r1 = r2 by A9, A8, Th18; :: thesis: verum
end;
now :: thesis: ( p = q implies r1 = r2 )
assume A10: p = q ; :: thesis: r1 = r2
then p = r1 by A1, A3, A5, Th17;
hence r1 = r2 by A1, A4, A6, A10, Th17; :: thesis: verum
end;
hence r1 = r2 by A7; :: thesis: verum