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