let N be non empty RelStr ; :: thesis: ( 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 )
:: thesis: ( RelStr(# the carrier of N,the InternalRel of N #) is transitive implies N is transitive )proof
assume A1:
N is
transitive
;
:: thesis: 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 #);
:: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume that A2:
x <= y
and A3:
y <= z
;
:: thesis: x <= z
reconsider x' =
x,
y' =
y,
z' =
z as
Element of
N ;
(
[x,y] in the
InternalRel of
RelStr(# the
carrier of
N,the
InternalRel of
N #) &
[y,z] in the
InternalRel of
RelStr(# the
carrier of
N,the
InternalRel of
N #) )
by A2, A3, ORDERS_2:def 9;
then
(
x' <= y' &
y' <= z' )
by ORDERS_2:def 9;
then
x' <= z'
by A1, 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;
:: thesis: verum
end;
assume A4:
RelStr(# the carrier of N,the InternalRel of N #) is transitive
; :: thesis: N is transitive
let x, y, z be Element of N; :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume that
A5:
x <= y
and
A6:
y <= z
; :: thesis: x <= z
reconsider x' = x, y' = y, z' = z as Element of RelStr(# the carrier of N,the InternalRel of N #) ;
( [x',y'] in the InternalRel of RelStr(# the carrier of N,the InternalRel of N #) & [y',z'] in the InternalRel of RelStr(# the carrier of N,the InternalRel of N #) )
by A5, A6, ORDERS_2:def 9;
then
( x' <= y' & y' <= z' )
by ORDERS_2:def 9;
then
x' <= z'
by 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; :: thesis: verum