theorem :: YELLOW_4:31

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)