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