theorem :: YELLOW_5:45

for L being non empty Boolean RelStr
for a, b being Element of L holds
( a \ b = Bottom L iff a <= b )