set J = the non empty upper-bounded Poset;
set x = the Element of L;
set M = the carrier of the non empty upper-bounded Poset --> the Element of L;
reconsider M = the carrier of the non empty upper-bounded Poset --> the Element of L as Function of the carrier of the non empty upper-bounded Poset, the carrier of L ;
set N = NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #);
A1: RelStr(# the carrier of NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #), the InternalRel of NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #) #) = RelStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset #) ;
[#] the non empty upper-bounded Poset = [#] NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #) ;
then [#] NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #) is directed by A1, Th3;
then reconsider N = NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #) as prenet of L by Def6;
take N ; :: thesis: ( N is monotone & N is antitone & N is strict )
thus N is monotone :: thesis: ( N is antitone & N is strict )

proof

let i, j be Element of N; :: according to ORDERS_3:def 5,WAYBEL_0:def 9 :: thesis: ( not i <= j or for b₁, b₂ being Element of the carrier of L holds
( not b₁ = (netmap (N,L)) . i or not b₂ = (netmap (N,L)) . j or b₁ <= b₂ ) )
assume i <= j ; :: thesis: for b₁, b₂ being Element of the carrier of L holds
( not b₁ = (netmap (N,L)) . i or not b₂ = (netmap (N,L)) . j or b₁ <= b₂ )
let a, b be Element of L; :: thesis: ( not a = (netmap (N,L)) . i or not b = (netmap (N,L)) . j or a <= b )
assume that
A2: a = (netmap (N,L)) . i and
A3: b = (netmap (N,L)) . j ; :: thesis: a <= b
A4: a = the Element of L by A2, FUNCOP_1:7;
the Element of L <= the Element of L ;
hence a <= b by A3, A4, FUNCOP_1:7; :: thesis: verum

end;

thus N is antitone :: thesis: N is strict

proof

let i, j be Element of N; :: according to WAYBEL_0:def 5,WAYBEL_0:def 10 :: thesis: ( i <= j implies for a, b being Element of L st a = (netmap (N,L)) . i & b = (netmap (N,L)) . j holds
a >= b )
assume i <= j ; :: thesis: for a, b being Element of L st a = (netmap (N,L)) . i & b = (netmap (N,L)) . j holds
a >= b
let a, b be Element of L; :: thesis: ( a = (netmap (N,L)) . i & b = (netmap (N,L)) . j implies a >= b )
assume that
A5: a = (netmap (N,L)) . i and
A6: b = (netmap (N,L)) . j ; :: thesis: a >= b
A7: a = the Element of L by A5, FUNCOP_1:7;
the Element of L <= the Element of L ;
hence a >= b by A6, A7, FUNCOP_1:7; :: thesis: verum

end;

thus N is strict ; :: thesis: verum