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 )

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

thus
N is antitone
:: thesis: N is strict
let i, j be Element of N; :: according to ORDERS_3:def 5,WAYBEL_0:def 9 :: thesis: ( not i <= j or for b_{1}, b_{2} being Element of the carrier of L holds

( not b_{1} = (netmap (N,L)) . i or not b_{2} = (netmap (N,L)) . j or b_{1} <= b_{2} ) )

assume i <= j ; :: thesis: for b_{1}, b_{2} being Element of the carrier of L holds

( not b_{1} = (netmap (N,L)) . i or not b_{2} = (netmap (N,L)) . j or b_{1} <= b_{2} )

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;( not b

assume i <= j ; :: thesis: for b

( not 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

proof

thus
N is strict
; :: thesis: verum
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;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