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

A2: now

assume a = b ; :: thesis: a,c '||' b,d
then ( a = b & c = d ) by A1, Th55;
hence a,c '||' b,d by PARSP_1:42; :: thesis: verum

end;

now

assume a <> b ; :: thesis: a,c '||' b,d
then ex p, q being Element of FdSp st
( parallelogram p,q,a,b & parallelogram p,q,c,d ) by A1, Def4;
hence a,c '||' b,d by Th47; :: thesis: verum

end;

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