for L being non empty Boolean RelStr
for a being Element of L holds
( a "/\" ('not' a) = Bottom L & a "\/" ('not' a) = Top L )