let K be non empty join-commutative join-associative ComplLLattStr ; :: thesis: ( K is Robbins implies K is Huntington )
assume A1: K is Robbins ; :: thesis: K is Huntington
then ex y, z being Element of K st y + z = z by Th58;
hence K is Huntington by A1, Th57; :: thesis: verum