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 Def18;
hence L is right-distributive by Def11; :: thesis: L is left-distributive
for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) by A1, Def18;
hence L is left-distributive by Def12; :: thesis: verum