let G be Abelian left-distributive doubleLoop; :: thesis: (- (1. G)) * (- (1. G)) = 1. G
thus (- (1. G)) * (- (1. G)) = - ((1_ G) * (- (1. G))) by Th7
.= - (- (1. G))
.= 1. G by Th3 ; :: thesis: verum