:: deftheorem defines # CARDFIL2:def 16 :
for L being RelStr
for x being Subset-Family of L holds # x = x;