set DM = DershowitzMannaOrder R;
thus
DershowitzMannaOrder R is asymmetric
DershowitzMannaOrder R is transitive proof
let a be
object ;
RELAT_2:def 5,
OPOSET_1:def 9 for b1 being object holds
( not a in the carrier of (DershowitzMannaOrder R) or not b1 in the carrier of (DershowitzMannaOrder R) or not [a,b1] in the InternalRel of (DershowitzMannaOrder R) or not [b1,a] in the InternalRel of (DershowitzMannaOrder R) )let b be
object ;
( not a in the carrier of (DershowitzMannaOrder R) or not b in the carrier of (DershowitzMannaOrder R) or not [a,b] in the InternalRel of (DershowitzMannaOrder R) or not [b,a] in the InternalRel of (DershowitzMannaOrder R) )
assume
(
a in the
carrier of
(DershowitzMannaOrder R) &
b in the
carrier of
(DershowitzMannaOrder R) )
;
( not [a,b] in the InternalRel of (DershowitzMannaOrder R) or not [b,a] in the InternalRel of (DershowitzMannaOrder R) )
then reconsider m =
a,
n =
b as
Element of
(DershowitzMannaOrder R) ;
assume
(
[a,b] in the
InternalRel of
(DershowitzMannaOrder R) &
[b,a] in the
InternalRel of
(DershowitzMannaOrder R) )
;
contradiction
then A0:
(
m <= n &
n <= m )
by ORDERS_2:def 5;
then
(
m <> n & ( for
a being
Element of
R st
m . a > n . a holds
ex
b being
Element of
R st
(
a <= b &
m . b < n . b ) ) & ( for
a being
Element of
R st
n . a > m . a holds
ex
b being
Element of
R st
(
a <= b &
n . b < m . b ) ) )
by HO;
then consider c being
object such that A2:
(
c in the
carrier of
R &
m . c <> n . c )
by PBOOLE:def 10;
reconsider c =
c as
Element of
R by A2;
set X =
{ d where d is Element of R : ( c <= d & m . d > n . d ) } ;
BC:
{ d where d is Element of R : ( c <= d & m . d > n . d ) } c= support m
ex
b being
Element of
R st
b in { d where d is Element of R : ( c <= d & m . d > n . d ) }
then consider d being
Element of
R such that A7:
d is_maximal_in { d where d is Element of R : ( c <= d & m . d > n . d ) }
by BC, Th12;
(
d in { d where d is Element of R : ( c <= d & m . d > n . d ) } & ( for
a being
Element of
R holds
( not
a in { d where d is Element of R : ( c <= d & m . d > n . d ) } or not
d < a ) ) )
by A7, WAYBEL_4:55;
then consider e being
Element of
R such that A8:
(
d = e &
c <= e &
n . e < m . e )
;
consider f being
Element of
R such that A9:
(
e <= f &
n . f > m . f )
by A0, HO, A8;
consider g being
Element of
R such that A10:
(
f <= g &
n . g < m . g )
by A0, HO, A9;
c <= f
by A8, A9, ORDERS_2:3;
then
(
c <= g &
d <= g )
by A8, A9, A10, ORDERS_2:3;
then
(
g in { d where d is Element of R : ( c <= d & m . d > n . d ) } &
d < g )
by A10, Lem2;
hence
contradiction
by A7, WAYBEL_4:55;
verum
end;
thus
DershowitzMannaOrder R is transitive
verumproof
let a,
b,
c be
object ;
RELAT_2:def 8,
ORDERS_2:def 3 ( not a in the carrier of (DershowitzMannaOrder R) or not b in the carrier of (DershowitzMannaOrder R) or not c in the carrier of (DershowitzMannaOrder R) or not [a,b] in the InternalRel of (DershowitzMannaOrder R) or not [b,c] in the InternalRel of (DershowitzMannaOrder R) or [a,c] in the InternalRel of (DershowitzMannaOrder R) )
assume
(
a in the
carrier of
(DershowitzMannaOrder R) &
b in the
carrier of
(DershowitzMannaOrder R) &
c in the
carrier of
(DershowitzMannaOrder R) )
;
( not [a,b] in the InternalRel of (DershowitzMannaOrder R) or not [b,c] in the InternalRel of (DershowitzMannaOrder R) or [a,c] in the InternalRel of (DershowitzMannaOrder R) )
then reconsider m =
a,
n =
b,
k =
c as
Element of
(DershowitzMannaOrder R) ;
assume
(
[a,b] in the
InternalRel of
(DershowitzMannaOrder R) &
[b,c] in the
InternalRel of
(DershowitzMannaOrder R) )
;
[a,c] in the InternalRel of (DershowitzMannaOrder R)
then A0:
(
m <= n &
n <= k )
by ORDERS_2:def 5;
consider x1,
y1 being
Element of
(DershowitzMannaOrder R) such that A2:
(
1. (DershowitzMannaOrder R) <> x1 &
x1 divides n &
m = (n -' x1) + y1 & ( for
b being
Element of
R st
y1 . b > 0 holds
ex
a being
Element of
R st
(
x1 . a > 0 &
b <= a ) ) )
by A0, DM;
consider x2,
y2 being
Element of
(DershowitzMannaOrder R) such that A3:
(
1. (DershowitzMannaOrder R) <> x2 &
x2 divides k &
n = (k -' x2) + y2 & ( for
b being
Element of
R st
y2 . b > 0 holds
ex
a being
Element of
R st
(
x2 . a > 0 &
b <= a ) ) )
by A0, DM;
reconsider x =
x2 + (x1 -' y2),
y =
(y2 -' x1) + y1 as
multiset of the
carrier of
R by Th1;
reconsider x =
x,
y =
y as
Element of
(DershowitzMannaOrder R) by Th2;
A4:
(
m = (((k -' x2) + y2) -' x1) + y1 &
(((k -' x2) + y2) -' x1) + y1 = (k -' x) + y )
by A2, A3, Th15;
A5:
1. (DershowitzMannaOrder R) <> x
A6:
x divides k
by A2, A3, Th15;
for
b being
Element of
R st
y . b > 0 holds
ex
a being
Element of
R st
(
x . a > 0 &
b <= a )
then
m <= k
by A4, A5, A6, DM;
hence
[a,c] in the
InternalRel of
(DershowitzMannaOrder R)
by ORDERS_2:def 5;
verum
end;