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