theorem :: ROBBINS1:37

for G being non empty join-commutative join-associative Robbins ComplLLattStr
for x, y being Element of G holds Expand (x,y) = y by Th36;