set Y = { [E,F] where E, F is Dependency of X : E <= F } ;
{ [E,F] where E, F is Dependency of X : E <= F } c= [:(Dependencies X),(Dependencies X):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [E,F] where E, F is Dependency of X : E <= F } or x in [:(Dependencies X),(Dependencies X):] )
assume x in { [E,F] where E, F is Dependency of X : E <= F } ; :: thesis: x in [:(Dependencies X),(Dependencies X):]
then ex E, F being Dependency of X st
( x = [E,F] & E <= F ) ;
hence x in [:(Dependencies X),(Dependencies X):] by ZFMISC_1:def 2; :: thesis: verum

end;

hence { [P,Q] where P, Q is Dependency of X : P <= Q } is Relation of (Dependencies X) ; :: thesis: verum