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 ( not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 ) ; :: thesis: r1 = r2
then ( not r1,p // r1,q & r1,r2 // r1,p & r1,r2 // r1,q ) by Th28;
hence r1 = r2 by Def1; :: thesis: verum