theorem :: ROBBINS1:34

for L being non empty ComplLLattStr
for a, b being Element of L
for a9, b9 being Element of (CLatt L) st a = a9 & b = b9 holds
( a *' b = a9 "/\" b9 & a + b = a9 "\/" b9 & a ` = a9 ` ) by Def11;