let K be non empty join-commutative join-associative ComplLattStr ; :: thesis: ( K is Robbins implies K is Huntington )
assume A1: K is Robbins ; :: thesis: K is Huntington
then consider y, z being Element of K such that
A2: y + z = z by Th60;
thus K is Huntington by A1, A2, Th59; :: thesis: verum