theorem :: ROBBINS3:29

for L being Ortholattice
for E being naturally_sup-generated CLatAugmentation of L holds E is Orthocomplemented by Th28;