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 Th33;
A1: for G being Dependency-set of X st F c= G & G is full_family holds
H c= G by Th37;
F c= H by Th37;
hence Dependency-closure F = X deps_encl_by (enclosure_of F) by A1, Def24; :: thesis: verum