for L being transitive antisymmetric with_infima RelStr
for N being prenet of L
for x being Element of L st N is eventually-directed holds
x "/\" N is eventually-directed