let FdSp be FanodesSp; :: thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c & parallelogram d,c,b,a )
let a, b, c, d be Element of FdSp; :: thesis: ( parallelogram a,b,c,d implies ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c & parallelogram d,c,b,a ) )
assume A1: parallelogram a,b,c,d ; :: thesis: ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c & parallelogram d,c,b,a )
then parallelogram c,d,a,b by Th39;
then A2: parallelogram c,a,d,b by Th38;
parallelogram b,a,d,c by A1, Th40;
hence ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c & parallelogram d,c,b,a ) by A1, A2, Th38, Th39; :: thesis: verum