:: deftheorem defines Tails CARDFIL2:def 14 :
for L being non empty RelStr holds Tails L = { (uparrow i) where i is Element of L : verum } ;