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 that
A2: a = (netmap (N,L)) . i and
A3: b = (netmap (N,L)) . j ; :: thesis: a <= b
A4: a = x by A2, FUNCOP_1:13;
x <= x ;
hence a <= b by A3, A4, FUNCOP_1:13; :: 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 = x by A5, FUNCOP_1:13;
x <= x ;
hence a >= b by A6, A7, FUNCOP_1:13; :: thesis: verum

end;

thus N is strict ; :: thesis: verum