:: deftheorem defines \\/ YELLOW_2:def 5 :
for L being non empty RelStr
for F being Relation holds \\/ (F,L) = "\/" ((rng F),L);