theorem Th50: :: YELLOW_7:50

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)) )