let G be non empty join-commutative join-associative Robbins ComplLLattStr ; :: thesis: ex y, z being Element of G st - (y + z) = - z
set x = the Element of G;
take y = the Element of G _1 ; :: thesis: ex z being Element of G st - (y + z) = - z
take z = the Element of G _3 ; :: thesis: - (y + z) = - z
- (y + z) = \delta ((\beta the Element of G), the Element of G) by Th53
.= - z by Th52 ;
hence - (y + z) = - z ; :: thesis: verum