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
; ( N is monotone & N is antitone & N is strict )
thus
N is monotone
( N is antitone & N is strict )proof
let i,
j be
Element of
N;
ORDERS_3:def 5,
WAYBEL_0:def 9 ( not i <= j or for b1, b2 being Element of the carrier of L holds
( not b1 = (netmap (N,L)) . i or not b2 = (netmap (N,L)) . j or b1 <= b2 ) )
assume
i <= j
;
for b1, b2 being Element of the carrier of L holds
( not b1 = (netmap (N,L)) . i or not b2 = (netmap (N,L)) . j or b1 <= b2 )
let a,
b be
Element of
L;
( 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
;
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;
verum
end;
thus
N is antitone
N is strict proof
let i,
j be
Element of
N;
WAYBEL_0:def 5,
WAYBEL_0:def 10 ( 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
;
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;
( 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
;
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;
verum
end;
thus
N is strict
; verum