theorem :: YELLOW_5:64

for L being non empty Boolean RelStr
for a being Element of L holds a \ a = Bottom L by Th34;