set N = L opp+id ;
thus
L opp+id is antitone
L opp+id is eventually-filtered proof
reconsider f =
id L as
Function of
(L ~),
L ;
reconsider g =
f as
Function of
L,
(L ~) ;
g is
antitone
by YELLOW_7:40;
then A1:
(
RelStr(# the
carrier of
L, the
InternalRel of
L #)
= RelStr(# the
carrier of
L, the
InternalRel of
L #) &
f is
antitone )
by YELLOW_7:41;
(
netmap (
(L opp+id),
L)
= id L &
RelStr(# the
carrier of
(L opp+id), the
InternalRel of
(L opp+id) #)
= RelStr(# the
carrier of
(L ~), the
InternalRel of
(L ~) #) )
by Def6, Th11;
hence
netmap (
(L opp+id),
L) is
antitone
by A1, Th2;
WAYBEL_0:def 10 verum
end;
for i being Element of (L opp+id) ex j being Element of (L opp+id) st
for k being Element of (L opp+id) st j <= k holds
(L opp+id) . i >= (L opp+id) . k
hence
L opp+id is eventually-filtered
by WAYBEL_0:12; verum