let N be non empty RelStr ; ( N is transitive iff RelStr(# the carrier of N,the InternalRel of N #) is transitive )
thus
( N is transitive implies RelStr(# the carrier of N,the InternalRel of N #) is transitive )
( RelStr(# the carrier of N,the InternalRel of N #) is transitive implies N is transitive )proof
assume A1:
N is
transitive
;
RelStr(# the carrier of N,the InternalRel of N #) is transitive
let x,
y,
z be
Element of ;
YELLOW_0:def 2 ( not x <= y or not y <= z or x <= z )
assume that A2:
x <= y
and A3:
y <= z
;
x <= z
reconsider x' =
x,
y' =
y,
z' =
z as
Element of ;
[y,z] in the
InternalRel of
RelStr(# the
carrier of
N,the
InternalRel of
N #)
by A3, ORDERS_2:def 9;
then A4:
y' <= z'
by ORDERS_2:def 9;
[x,y] in the
InternalRel of
RelStr(# the
carrier of
N,the
InternalRel of
N #)
by A2, ORDERS_2:def 9;
then
x' <= y'
by ORDERS_2:def 9;
then
x' <= z'
by A1, A4, YELLOW_0:def 2;
then
[x',z'] in the
InternalRel of
N
by ORDERS_2:def 9;
hence
x <= z
by ORDERS_2:def 9;
verum
end;
assume A5:
RelStr(# the carrier of N,the InternalRel of N #) is transitive
; N is transitive
let x, y, z be Element of ; YELLOW_0:def 2 ( not x <= y or not y <= z or x <= z )
assume that
A6:
x <= y
and
A7:
y <= z
; x <= z
reconsider x' = x, y' = y, z' = z as Element of ;
[y',z'] in the InternalRel of RelStr(# the carrier of N,the InternalRel of N #)
by A7, ORDERS_2:def 9;
then A8:
y' <= z'
by ORDERS_2:def 9;
[x',y'] in the InternalRel of RelStr(# the carrier of N,the InternalRel of N #)
by A6, ORDERS_2:def 9;
then
x' <= y'
by ORDERS_2:def 9;
then
x' <= z'
by A5, A8, YELLOW_0:def 2;
then
[x,z] in the InternalRel of N
by ORDERS_2:def 9;
hence
x <= z
by ORDERS_2:def 9; verum