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 set ; :: 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 consider E, F being Dependency of X such that
A1: x = [E,F] and
E <= F ;
thus x in [:(Dependencies X),(Dependencies X):] by A1, 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