:: deftheorem defines deps_encl_by ARMSTRNG:def 22 :
for X, B being set holds X deps_encl_by B = { [a,b] where a, b is Subset of X : for c being set st c in B & a c= c holds
b c= c } ;