let R be RelStr ; ( R is total implies R is serial )
set RR = the InternalRel of R;
set X = the carrier of R;
assume
R is total
; R is serial
then A1:
dom the InternalRel of R = the carrier of R
by PARTFUN1:def 2;
the InternalRel of R is_serial_in the carrier of R
proof
let x be
object ;
ROUGHS_2:def 1 ( x in the carrier of R implies ex y being object st
( y in the carrier of R & [x,y] in the InternalRel of R ) )
assume
x in the
carrier of
R
;
ex y being object st
( y in the carrier of R & [x,y] in the InternalRel of R )
then consider y being
object such that A2:
[x,y] in the
InternalRel of
R
by A1, RELSET_1:9;
take
y
;
( y in the carrier of R & [x,y] in the InternalRel of R )
consider xx,
yy being
object such that A3:
(
[x,y] = [xx,yy] &
xx in the
carrier of
R &
yy in the
carrier of
R )
by A2, RELSET_1:2;
thus
(
y in the
carrier of
R &
[x,y] in the
InternalRel of
R )
by A2, A3, XTUPLE_0:1;
verum
end;
hence
R is serial
; verum