let X be non empty finite set ; :: thesis: for F being Dependency-set of X holds
( enclosure_of F is (B1) & enclosure_of F is (B2) )
let F be Dependency-set of X; :: thesis: ( enclosure_of F is (B1) & enclosure_of F is (B2) )
set B = enclosure_of F;
A1: for x, y being Subset of st [x,y] in F & x c= X holds
y c= X ;
X = [#] X ;
then X in enclosure_of F by A1;
hence enclosure_of F is (B1) by Def4; :: thesis: enclosure_of F is (B2)
let a, b be set ; :: according to FINSUB_1:def 2 :: thesis: ( not a in enclosure_of F or not b in enclosure_of F or a /\ b in enclosure_of F )
assume that
A2: a in enclosure_of F and
A3: b in enclosure_of F ; :: thesis: a /\ b in enclosure_of F
consider b' being Subset of such that
A4: b' = b and
A5: for x, y being Subset of st [x,y] in F & x c= b' holds
y c= b' by A3;
consider a' being Subset of such that
A6: a' = a and
A7: for x, y being Subset of st [x,y] in F & x c= a' holds
y c= a' by A2;
reconsider ab = a' /\ b' as Subset of ;

now

let x, y be Subset of ; :: thesis: ( [x,y] in F & x c= ab implies y c= ab )
assume that
A8: [x,y] in F and
A9: x c= ab ; :: thesis: y c= ab
A10: y c= b' by A5, A8, A9, XBOOLE_1:18;
y c= a' by A7, A8, A9, XBOOLE_1:18;
hence y c= ab by A10, XBOOLE_1:19; :: thesis: verum

end;

hence a /\ b in enclosure_of F by A6, A4; :: thesis: verum