:: deftheorem defines Bottom YELLOW_0:def 11 :
for L being RelStr holds Bottom L = "\/" ({},L);