let FdSp be FanodesSp; :: thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
a,b congr c,d
let a, b, c, d be Element of FdSp; :: thesis: ( parallelogram a,b,c,d implies a,b congr c,d )
A1: a,b '||' a,b by PARSP_1:25;
assume A2: parallelogram a,b,c,d ; :: thesis: a,b congr c,d
then A3: ( not a,c,b is_collinear & a <> b ) by Th34, Th36;
a <> c by A2, Th34;
then consider p being Element of FdSp such that
A4: a,c,p is_collinear and
A5: a <> p and
A6: c <> p by Th46;
a,c '||' a,p by A4, Def2;
then consider q being Element of FdSp such that
A7: parallelogram a,p,b,q by A5, A1, A3, Th17, Th42;
parallelogram a,b,p,q by A7, Th41;
then parallelogram c,d,p,q by A2, A4, A6, Th49;
then A8: parallelogram p,q,c,d by Th41;
parallelogram p,q,a,b by A7, Th41;
hence a,b congr c,d by A8, Def4; :: thesis: verum