set at = the Attributes of R;
set X = { [A,B] where A, B is Subset of the Attributes of R : A >|> B,R } ;
{ [A,B] where A, B is Subset of the Attributes of R : A >|> B,R } c= [:(bool the Attributes of R),(bool the Attributes of R):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [A,B] where A, B is Subset of the Attributes of R : A >|> B,R } or x in [:(bool the Attributes of R),(bool the Attributes of R):] )
assume x in { [A,B] where A, B is Subset of the Attributes of R : A >|> B,R } ; :: thesis: x in [:(bool the Attributes of R),(bool the Attributes of R):]
then ex A, B being Subset of the Attributes of R st
( x = [A,B] & A >|> B,R ) ;
hence x in [:(bool the Attributes of R),(bool the Attributes of R):] by ZFMISC_1:def 2; :: thesis: verum

end;

hence { [A,B] where A, B is Subset of the Attributes of R : A >|> B,R } is Dependency-set of the Attributes of R ; :: thesis: verum