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 :: thesis: ( a = b implies a,c '||' b,d )
assume A3: a = b ; :: thesis: a,c '||' b,d
then c = d by A1, Th45;
hence a,c '||' b,d by A3, PARSP_1:25; :: thesis: verum
end;
( a <> b implies a,c '||' b,d ) by A1, Th39;
hence a,c '||' b,d by A2; :: thesis: verum