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
RelStr(# the
carrier of
N, the
InternalRel of
N #);
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 x9 =
x,
y9 =
y,
z9 =
z as
Element of
N ;
[y,z] in the
InternalRel of
RelStr(# the
carrier of
N, the
InternalRel of
N #)
by A3, ORDERS_2:def 5;
then A4:
y9 <= z9
by ORDERS_2:def 5;
[x,y] in the
InternalRel of
RelStr(# the
carrier of
N, the
InternalRel of
N #)
by A2, ORDERS_2:def 5;
then
x9 <= y9
by ORDERS_2:def 5;
then
x9 <= z9
by A1, A4;
then
[x9,z9] in the
InternalRel of
N
by ORDERS_2:def 5;
hence
x <= z
by ORDERS_2:def 5;
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 N; 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 x9 = x, y9 = y, z9 = z as Element of RelStr(# the carrier of N, the InternalRel of N #) ;
[y9,z9] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #)
by A7, ORDERS_2:def 5;
then A8:
y9 <= z9
by ORDERS_2:def 5;
[x9,y9] in the InternalRel of RelStr(# the carrier of N, the InternalRel of N #)
by A6, ORDERS_2:def 5;
then
x9 <= y9
by ORDERS_2:def 5;
then
x9 <= z9
by A5, A8;
then
[x,z] in the InternalRel of N
by ORDERS_2:def 5;
hence
x <= z
by ORDERS_2:def 5; verum