let X be set ; :: thesis: field (Dependencies-Order X) = [:(bool X),(bool X):]
thus field (Dependencies-Order X) = (dom (Dependencies-Order X)) \/ (rng (Dependencies-Order X)) by RELAT_1:def 6
.= [:(bool X),(bool X):] \/ (rng (Dependencies-Order X)) by Th15
.= [:(bool X),(bool X):] \/ [:(bool X),(bool X):] by Th16
.= [:(bool X),(bool X):] ; :: thesis: verum