let SAS be Semi_Affine_Space; :: thesis: for a, b, c, p, r being Element of SAS st not a,b // a,c & a,c // p,r & b,c // p,r holds
p = r
let a, b, c, p, r be Element of SAS; :: thesis: ( not a,b // a,c & a,c // p,r & b,c // p,r implies p = r )
assume ( not a,b // a,c & a,c // p,r & b,c // p,r ) ; :: thesis: p = r
then ( not a,c // b,c & p,r // a,c & p,r // b,c ) by Th17, Th28;
hence p = r by Def1; :: thesis: verum