for L being non empty antisymmetric complete RelStr
for F being Function-yielding Function holds
( \// (F,L) = /\\ (F,(L opp)) & /\\ (F,L) = \// (F,(L opp)) )