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

now :: thesis: for x, y being Subset of X st [x,y] in F & x c= ab holds
y c= ab

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
A10: y c= b9 by A5, A8, A9, XBOOLE_1:18;
y c= a9 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