for GX being non empty TopSpace
for B being Subset of GX
for V being Subset of (GX | B) st V c= B holds
Down ((Up V),B) = V by XBOOLE_1:28;