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 Th1;
assume A2: parallelogram a,b,c,d ; :: thesis: congr a,b,c,d
then A3: ( not a,c,b are_collinear & a <> b ) by Th36, Th38;
a <> c by A2, Th36;
then consider p being Element of SAS such that
A4: a,c,p are_collinear and
A5: a <> p and
A6: c <> p by Th48;
a,c // a,p by A4;
then consider q being Element of SAS such that
A7: parallelogram a,p,b,q by A5, A1, A3, Th23, Th44;
parallelogram a,b,p,q by A7, Th43;
then parallelogram c,d,p,q by A2, A4, A6, Th51;
then A8: parallelogram p,q,c,d by Th43;
parallelogram p,q,a,b by A7, Th43;
hence congr a,b,c,d by A8; :: thesis: verum