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: X = [#] X ;
for x, y being Subset of X st [x,y] in F & x c= X holds
y c= 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 a' being Subset of X such that
A4: a' = a and
A5: for x, y being Subset of X st [x,y] in F & x c= a' holds
y c= a' by A2;
consider b' being Subset of X such that
A6: b' = b and
A7: for x, y being Subset of X st [x,y] in F & x c= b' holds
y c= b' by A3;
reconsider ab = a' /\ b' as Subset of X ;

now

let x, y be Subset of X; :: 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
( x c= a' & x c= b' ) by A9, XBOOLE_1:18;
then ( y c= a' & y c= b' ) by A5, A7, A8;
hence y c= ab by XBOOLE_1:19; :: thesis: verum

end;

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