set F = { [a,b] where a, b is Subset of X : for c being set st c in B & a c= c holds
b c= c } ;
{ [a,b] where a, b is Subset of X : for c being set st c in B & a c= c holds
b c= c } c= [:(bool X),(bool X):]

proof

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

end;

hence { [a,b] where a, b is Subset of X : for c being set st c in B & a c= c holds
b c= c } is Dependency-set of X ; :: thesis: verum