let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d being Element of SAS st parallelogram a,b,c,d holds
congr a,b,c,d
let a, b, c, d be Element of SAS; :: thesis: ( parallelogram a,b,c,d implies congr a,b,c,d )
A1: a,b // a,b by Th12;
assume A2: parallelogram a,b,c,d ; :: thesis: congr a,b,c,d
then A3: ( not a,c,b is_collinear & a <> b ) by Th54, Th56;
a <> c by A2, Th54;
then consider p being Element of SAS such that
A4: a,c,p is_collinear and
A5: a <> p and
A6: c <> p by Th66;
a,c // a,p by A4, Def2;
then consider q being Element of SAS such that
A7: parallelogram a,p,b,q by A5, A1, A3, Th39, Th62;
parallelogram a,b,p,q by A7, Th61;
then parallelogram c,d,p,q by A2, A4, A6, Th69;
then A8: parallelogram p,q,c,d by Th61;
parallelogram p,q,a,b by A7, Th61;
hence congr a,b,c,d by A8, Def4; :: thesis: verum