set B = { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } ;
A1: { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } = enclosure_of F ;
{ c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } c= bool X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } or x in bool X )
assume x in { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } ; :: thesis: x in bool X
then ex c being Subset of X st
( x = c & ( for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c ) ) ;
hence x in bool X ; :: thesis: verum

end;

then reconsider B = { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } as Subset-Family of X ;
set H = X deps_encl_by B;
reconsider H = X deps_encl_by B as Full-family of X by Th33;
take H ; :: thesis: ( F c= H & ( for G being Dependency-set of X st F c= G & G is full_family holds
H c= G ) )
thus ( F c= H & ( for G being Dependency-set of X st F c= G & G is full_family holds
H c= G ) ) by A1, Th37; :: thesis: verum