consider J being non empty upper-bounded Poset;
consider x being Element of L;
set M = the carrier of J --> x;
reconsider M = the carrier of J --> x as Function of the carrier of J,the carrier of L ;
set N = NetStr(# the carrier of J,the InternalRel of J,M #);
A1: RelStr(# the carrier of NetStr(# the carrier of J,the InternalRel of J,M #),the InternalRel of NetStr(# the carrier of J,the InternalRel of J,M #) #) = RelStr(# the carrier of J,the InternalRel of J #) ;
[#] J = [#] NetStr(# the carrier of J,the InternalRel of J,M #) ;
then [#] NetStr(# the carrier of J,the InternalRel of J,M #) is directed by A1, Th3;
then reconsider N = NetStr(# the carrier of J,the InternalRel of J,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 ( a = (netmap N,L) . i & b = (netmap N,L) . j ) ; :: thesis: a <= b
then ( a = x & b = x & x <= x ) by FUNCOP_1:13;
hence a <= b ; :: 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 ( a = (netmap N,L) . i & b = (netmap N,L) . j ) ; :: thesis: a >= b
then ( a = x & b = x & x <= x ) by FUNCOP_1:13;
hence a >= b ; :: thesis: verum

end;

thus N is strict ; :: thesis: verum