set N = L opp+id ;
thus
L opp+id is antitone
:: thesis: L opp+id is eventually-filtered proof
A1:
netmap (L opp+id ),
L = id L
by Def6;
A2:
RelStr(# the
carrier of
(L opp+id ),the
InternalRel of
(L opp+id ) #)
= RelStr(# the
carrier of
(L ~ ),the
InternalRel of
(L ~ ) #)
by Th11;
reconsider f =
id L as
Function of
(L ~ ),
L ;
reconsider g =
f as
Function of
L,
(L ~ ) ;
A3:
RelStr(# the
carrier of
L,the
InternalRel of
L #)
= RelStr(# the
carrier of
L,the
InternalRel of
L #)
;
g is
antitone
by YELLOW_7:40;
then
f is
antitone
by YELLOW_7:41;
hence
netmap (L opp+id ),
L is
antitone
by A1, A2, A3, Th2;
:: according to WAYBEL_0:def 10 :: thesis: 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; :: thesis: verum