let X be non empty finite set ; :: thesis: for F being Dependency-set of X holds Dependency-closure F = X deps_encl_by (enclosure_of F)
let F be Dependency-set of X; :: thesis: Dependency-closure F = X deps_encl_by (enclosure_of F)
set B = enclosure_of F;
set H = X deps_encl_by (enclosure_of F);
reconsider H = X deps_encl_by (enclosure_of F) as Full-family of X by Th35;
A1: F c= H by Th39;
for G being Dependency-set of X st F c= G & G is full_family holds
H c= G by Th39;
hence Dependency-closure F = X deps_encl_by (enclosure_of F) by A1, Def25; :: thesis: verum