let SAS be Semi_Affine_Space; :: thesis: for p, q, r1, r2 being Element of SAS st not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 holds
r1 = r2
let p, q, r1, r2 be Element of SAS; :: thesis: ( not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 implies r1 = r2 )
assume that
A1: ( not p,q // p,r1 & p,r1 // p,r2 ) and
A2: q,r1 // q,r2 ; :: thesis: r1 = r2
A3: r1,r2 // r1,q by A2, Th14;
( not r1,p // r1,q & r1,r2 // r1,p ) by A1, Th14;
hence r1 = r2 by A3, Def1; :: thesis: verum