let FdSp be FanodesSp; :: thesis: for a, b, c, d, r, s being Element of FdSp st a,b congr c,d & a,b,c are_collinear & parallelogram r,s,a,b holds
parallelogram r,s,c,d
let a, b, c, d, r, s be Element of FdSp; :: thesis: ( a,b congr c,d & a,b,c are_collinear & parallelogram r,s,a,b implies parallelogram r,s,c,d )
assume that
A1: a,b congr c,d and
A2: a,b,c are_collinear and
A3: parallelogram r,s,a,b ; :: thesis: parallelogram r,s,c,d
now :: thesis: ( a <> b implies parallelogram r,s,c,d )
assume A4: a <> b ; :: thesis: parallelogram r,s,c,d
then consider p, q being Element of FdSp such that
A5: parallelogram p,q,a,b and
A6: parallelogram p,q,c,d by A1;
( r,s '||' a,b & a,b '||' c,d ) by A1, A3, Th48;
then A7: r,s '||' c,d by A4, PARSP_1:26;
A8: parallelogram a,b,r,s by A3, Th33;
parallelogram a,b,p,q by A5, Th33;
then A9: r,c '||' s,d by A6, A8, Th42;
not r,s,c are_collinear by A2, A3, Th29;
hence parallelogram r,s,c,d by A7, A9; :: thesis: verum
end;
hence parallelogram r,s,c,d by A3, Th26; :: thesis: verum