let R be non empty reflexive transitive RelStr ; :: thesis: for x, y being Element of R st the InternalRel of R reduces x,y holds
[x,y] in the InternalRel of R
let x, y be Element of R; :: thesis: ( the InternalRel of R reduces x,y implies [x,y] in the InternalRel of R )
set cR = the carrier of R;
set IR = the InternalRel of R;
assume A1:
the InternalRel of R reduces x,y
; :: thesis: [x,y] in the InternalRel of R
A2:
the InternalRel of R is_reflexive_in the carrier of R
by ORDERS_2:def 4;
A3:
the InternalRel of R is_transitive_in the carrier of R
by ORDERS_2:def 5;
consider p being RedSequence of the InternalRel of R such that
A4:
( p . 1 = x & p . (len p) = y )
by A1, REWRITE1:def 3;
reconsider p = p as FinSequence ;
A5:
( len p > 0 & ( for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in the InternalRel of R ) )
by REWRITE1:def 2;
then
0 + 1 <= len p
by NAT_1:13;
then A6:
len p in dom p
by FINSEQ_3:27;
defpred S1[ Nat] means ( $1 in dom p implies [(p . 1),(p . $1)] in the InternalRel of R );
A7:
S1[1]
by A2, A4, RELAT_2:def 1;
A8:
for k being non empty Nat st S1[k] holds
S1[k + 1]
proof
let k be non
empty Nat;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A9:
S1[
k]
;
:: thesis: S1[k + 1]
assume A10:
k + 1
in dom p
;
:: thesis: [(p . 1),(p . (k + 1))] in the InternalRel of R
A11:
k <= k + 1
by NAT_1:11;
A12:
0 + 1
<= k
by NAT_1:13;
k + 1
<= len p
by A10, FINSEQ_3:27;
then A13:
( 1
<= k &
k <= len p )
by A11, A12, XXREAL_0:2;
then
k in dom p
by FINSEQ_3:27;
then
[(p . k),(p . (k + 1))] in the
InternalRel of
R
by A10, REWRITE1:def 2;
then
(
p . 1
in the
carrier of
R &
p . k in the
carrier of
R &
p . (k + 1) in the
carrier of
R &
[(p . 1),(p . k)] in the
InternalRel of
R &
[(p . k),(p . (k + 1))] in the
InternalRel of
R )
by A9, A13, FINSEQ_3:27, ZFMISC_1:106;
hence
[(p . 1),(p . (k + 1))] in the
InternalRel of
R
by A3, RELAT_2:def 8;
:: thesis: verum
end;
for k being non empty Nat holds S1[k]
from NAT_1:sch 10(A7, A8);
hence
[x,y] in the InternalRel of R
by A4, A5, A6; :: thesis: verum