let L be non empty doubleLoopStr ; :: thesis: ( L is distributive implies ( L is right-distributive & L is left-distributive ) )
assume A1: L is distributive ; :: thesis: ( L is right-distributive & L is left-distributive )
then for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) by Def7;
hence L is right-distributive by Def2; :: thesis: L is left-distributive
for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) by A1, Def7;
hence L is left-distributive by Def3; :: thesis: verum