theorem :: YELLOW_4:60

for L being non empty RelStr
for D being Subset of [:L,L:] holds union { X where X is Subset of L : ex x being Element of L st
( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D)