let SAS be Semi_Affine_Space; :: thesis: for a, b, c, p, q, r being Element of SAS st not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p <> q holds
not p,q // p,r
let a, b, c, p, q, r be Element of SAS; :: thesis: ( not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p <> q implies not p,q // p,r )
assume that
A1: not a,b // a,c and
A2: a,b // p,q and
A3: a,c // p,r and
A4: b,c // q,r and
A5: p <> q ; :: thesis: not p,q // p,r
now :: thesis: not p = r
assume p = r ; :: thesis: contradiction
then A6: p,q // b,c by A4, Th6;
p,q // a,b by A2, Th6;
then a,b // b,c by A5, A6, Def1;
then b,a // b,c by Th4;
hence contradiction by A1, Th7; :: thesis: verum
end;
hence not p,q // p,r by A1, A2, A3, A5, Th15; :: thesis: verum