:: deftheorem defines is_tail_of CALCUL_1:def 3 :
for f being Relation
for p being set holds
( p is_tail_of f iff p in rng f );