let SAS be Semi_Affine_Space; :: thesis: for a, a', b, b', c, c' being Element of SAS st parallelogram a,a',b,b' & parallelogram a,a',c,c' holds
b,c // b',c'
let a, a', b, b', c, c' be Element of SAS; :: thesis: ( parallelogram a,a',b,b' & parallelogram a,a',c,c' implies b,c // b',c' )
assume ( parallelogram a,a',b,b' & parallelogram a,a',c,c' ) ; :: thesis: b,c // b',c'
then ( not a,a',b is_collinear & not a,a',c is_collinear & a,a' // b,b' & a,b // a',b' & a,a' // c,c' & a,c // a',c' ) by Def3;
then ( not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,b // a',b' & a,a' // c,c' & a,c // a',c' ) by Def2;
hence b,c // b',c' by Def1; :: thesis: verum