let PS be ParSp; :: thesis: for a, b, c, d, p, q, r, s being Element of PS 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 PS; :: 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, Th26;
then A6: r,s '||' a,b by Th23;
r,s '||' c,d by A3, Th23;
hence contradiction by A1, A5, A6, Def11; :: thesis: verum