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 that
A1: parallelogram a,a',b,b' and
A2: parallelogram a,a',c,c' ; :: thesis: b,c // b',c'
A3: ( a,a' // c,c' & a,c // a',c' ) by A2, Def3;
not a,a',c is_collinear by A2, Def3;
then A4: not a,a' // a,c by Def2;
not a,a',b is_collinear by A1, Def3;
then A5: not a,a' // a,b by Def2;
( a,a' // b,b' & a,b // a',b' ) by A1, Def3;
hence b,c // b',c' by A5, A4, A3, Def1; :: thesis: verum