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