let FdSp be FanodesSp; :: thesis: for a, b, c, d being Element of FdSp st a,b congr c,d holds
a,b '||' c,d
let a, b, c, d be Element of FdSp; :: thesis: ( a,b congr c,d implies a,b '||' c,d )
assume A1: a,b congr c,d ; :: thesis: a,b '||' c,d

now :: thesis: ( a <> b implies a,b '||' c,d )

assume a <> b ; :: thesis: a,b '||' c,d
then consider p, q being Element of FdSp such that
A2: parallelogram p,q,a,b and
A3: parallelogram p,q,c,d by A1;
A4: p,q '||' c,d by A3;
( p <> q & p,q '||' a,b ) by A2, Th26;
hence a,b '||' c,d by A4, PARSP_1:def 12; :: thesis: verum

end;

hence a,b '||' c,d by PARSP_1:20; :: thesis: verum