set N = L opp+id ;
thus L opp+id is antitone :: thesis: 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; :: 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

proof

let i be Element of (L opp+id); :: thesis: 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
take j = i; :: thesis: for k being Element of (L opp+id) st j <= k holds
(L opp+id) . i >= (L opp+id) . k
A2: ( the mapping of (L opp+id) = id L & the InternalRel of (L opp+id) = the InternalRel of L ~ ) by Def6;
let k be Element of (L opp+id); :: thesis: ( j <= k implies (L opp+id) . i >= (L opp+id) . k )
assume j <= k ; :: thesis: (L opp+id) . i >= (L opp+id) . k
then [i,k] in the InternalRel of (L opp+id) ;
then A3: [k,i] in the InternalRel of (L opp+id) ~ by RELAT_1:def 7;
reconsider i1 = i, k1 = k as Element of L by Def6;
( (id L) . i1 = i1 & (id L) . k1 = k1 ) ;
hence (L opp+id) . i >= (L opp+id) . k by A2, A3; :: thesis: verum

end;

hence L opp+id is eventually-filtered by WAYBEL_0:12; :: thesis: verum