for L being non empty antisymmetric RelStr st ( L is with_suprema or L is with_infima ) holds
for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds
X /\ Y is filtered