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

now

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

end;

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