let SAS be Semi_Affine_Space; 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; ( 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
; 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; verum