let SAS be Semi_Affine_Space; :: thesis: for a, a9, b, b9, c, c9 being Element of SAS st parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 holds
b,c // b9,c9
let a, a9, b, b9, c, c9 be Element of SAS; :: thesis: ( parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 implies b,c // b9,c9 )
assume that
A1: parallelogram a,a9,b,b9 and
A2: parallelogram a,a9,c,c9 ; :: thesis: b,c // b9,c9
A3: ( a,a9 // c,c9 & a,c // a9,c9 ) by A2;
not a,a9,c are_collinear by A2;
then A4: not a,a9 // a,c ;
not a,a9,b are_collinear by A1;
then A5: not a,a9 // a,b ;
( a,a9 // b,b9 & a,b // a9,b9 ) by A1;
hence b,c // b9,c9 by A5, A4, A3, Def1; :: thesis: verum