let X be set ; :: thesis: rng (Dependencies-Order X) = [:(bool X),(bool X):]
now :: thesis: for x being object holds
( ( 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) ) )
let x be object ; :: 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 XTUPLE_0:def 13; :: thesis: verum
end;
hence rng (Dependencies-Order X) = [:(bool X),(bool X):] by TARSKI:2; :: thesis: verum