set X = { [A,B] where A, B is Subset of the Attributes of R : A >|> B,R } ;
set at = the Attributes of 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 set ; :: 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 consider A, B being Subset of the Attributes of R such that
A1: x = [A,B] and
A >|> B,R ;
thus x in [:(bool the Attributes of R),(bool the Attributes of R):] by A1, 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