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 Th26, Th28;
a <> c by A2, Th26;
then consider p being Element of FdSp such that
A4: a,c,p is_collinear and
A5: a <> p and
A6: c <> p by Th38;
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, Th11, Th34;
parallelogram a,b,p,q by A7, Th33;
then parallelogram c,d,p,q by A2, A4, A6, Th41;
then A8: parallelogram p,q,c,d by Th33;
parallelogram p,q,a,b by A7, Th33;
hence a,b congr c,d by A8, Def4; :: thesis: verum