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 } )