theorem Th4: :: YELLOW_9:4

for R being non empty RelStr
for F being Subset of R holds
( uparrow F = union { (uparrow x) where x is Element of R : x in F } & downarrow F = union { (downarrow x) where x is Element of R : x in F } )