let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d, r, s being Element of SAS st congr r,s,a,b & congr r,s,c,d holds
congr a,b,c,d
let a, b, c, d, r, s be Element of SAS; :: thesis: ( congr r,s,a,b & congr r,s,c,d implies congr a,b,c,d )
assume that
A1: congr r,s,a,b and
A2: congr r,s,c,d ; :: thesis: congr a,b,c,d
A3: now :: thesis: ( r <> s & not r,s,a are_collinear & not r,s,c are_collinear implies congr a,b,c,d )
assume that
r <> s and
A4: ( not r,s,a are_collinear & not r,s,c are_collinear ) ; :: thesis: congr a,b,c,d
( parallelogram r,s,a,b & parallelogram r,s,c,d ) by A1, A2, A4, Th59;
hence congr a,b,c,d ; :: thesis: verum
end;
A5: now :: thesis: ( r <> s & r,s,c are_collinear implies congr a,b,c,d )
assume that
A6: r <> s and
A7: r,s,c are_collinear ; :: thesis: congr a,b,c,d
consider p, q being Element of SAS such that
A8: parallelogram p,q,r,s and
A9: parallelogram p,q,a,b by A1, A6;
parallelogram p,q,c,d by A2, A7, A8, Th61;
hence congr a,b,c,d by A9; :: thesis: verum
end;
A10: now :: thesis: ( r <> s & r,s,a are_collinear implies congr a,b,c,d )
assume that
A11: r <> s and
A12: r,s,a are_collinear ; :: thesis: congr a,b,c,d
consider p, q being Element of SAS such that
A13: parallelogram p,q,r,s and
A14: parallelogram p,q,c,d by A2, A11;
parallelogram p,q,a,b by A1, A12, A13, Th61;
hence congr a,b,c,d by A14; :: thesis: verum
end;
( r = s implies congr a,b,c,d ) by A1, A2, Th54;
hence congr a,b,c,d by A10, A5, A3; :: thesis: verum