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