theorem Th49: :: YELLOW_7:49

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