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

now :: thesis: for x being object holds
( ( 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) ) )

let x be object ; :: 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 XTUPLE_0:def 12; :: thesis: verum

end;

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