let X be set ; :: thesis: rng (Dependencies-Order X) = [:(bool X),(bool X):]

now

let x be set ; :: thesis: ( ( x in rng (Dependencies-Order X) implies x in [:(bool X),(bool X):] ) & ( x in [:(bool X),(bool X):] implies x in rng (Dependencies-Order X) ) )
thus ( x in rng (Dependencies-Order X) implies x in [:(bool X),(bool X):] ) ; :: thesis: ( x in [:(bool X),(bool X):] implies x in rng (Dependencies-Order X) )
assume x in [:(bool X),(bool X):] ; :: thesis: x in rng (Dependencies-Order X)
then reconsider x9 = x as Dependency of X ;
[x9,x9] in Dependencies-Order X ;
hence x in rng (Dependencies-Order X) by RELAT_1:def 5; :: thesis: verum

end;

hence rng (Dependencies-Order X) = [:(bool X),(bool X):] by TARSKI:1; :: thesis: verum