let R be RelStr ; :: thesis: ( R is total implies R is serial )
set RR = the InternalRel of R;
set X = the carrier of R;
assume R is total ; :: thesis: 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 ; :: according to ROUGHS_2:def 1 :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum

end;

hence R is serial ; :: thesis: verum