for S being non empty Poset
for N being reflexive monotone net of S holds { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } is non empty directed Subset of S