let FdSp be FanodesSp; :: thesis: for p, q being Element of FdSp st p <> q holds
ex r being Element of FdSp st not p,q '||' p,r
let p, q be Element of FdSp; :: thesis: ( p <> q implies ex r being Element of FdSp st not p,q '||' p,r )
assume A1: p <> q ; :: thesis: not for r being Element of FdSp holds p,q '||' p,r
consider a, b, c being Element of FdSp such that
A2: not a,b '||' a,c by Def1;
( not p,q '||' p,a or not p,q '||' p,b or not p,q '||' p,c ) by A1, A2, PARSP_1:56;
hence not for r being Element of FdSp holds p,q '||' p,r ; :: thesis: verum