let FdSp be FanodesSp; 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; ( 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
; ( 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 Th31;
then A2:
parallelogram c,a,d,b
by Th30;
parallelogram b,a,d,c
by A1, Th32;
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, Th30, Th31; verum