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