let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d, r, s being Element of SAS st congr a,b,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 SAS; :: thesis: ( congr a,b,c,d & a,b,c are_collinear & parallelogram r,s,a,b implies parallelogram r,s,c,d )
assume that
A1: congr a,b,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 )
A4: parallelogram a,b,r,s by A3, Th43;
assume A5: a <> b ; :: thesis: parallelogram r,s,c,d
then consider p, q being Element of SAS such that
A6: parallelogram p,q,a,b and
A7: parallelogram p,q,c,d by A1;
parallelogram a,b,p,q by A6, Th43;
then A8: r,c // s,d by A7, A4, Th52;
( r,s // a,b & a,b // c,d ) by A1, A3, Th57;
then A9: r,s // c,d by A5, Th8;
not r,s,c are_collinear by A2, A3, Th39;
hence parallelogram r,s,c,d by A9, A8; :: thesis: verum
end;
hence parallelogram r,s,c,d by A3, Th36; :: thesis: verum