let R be RelStr ; :: thesis: ( R is serial implies R is total )
set RR = the InternalRel of R;
set X = the carrier of R;
assume A4: R is serial ; :: thesis: R is total
for x being object st x in the carrier of R holds
ex y being object st [x,y] in the InternalRel of R
proof
let x be object ; :: thesis: ( x in the carrier of R implies ex y being object st [x,y] in the InternalRel of R )
assume x in the carrier of R ; :: thesis: ex y being object st [x,y] in the InternalRel of R
then ex y being object st
( y in the carrier of R & [x,y] in the InternalRel of R ) by Def1, A4;
hence ex y being object st [x,y] in the InternalRel of R ; :: thesis: verum
end;
then dom the InternalRel of R = the carrier of R by RELSET_1:9;
then the InternalRel of R is total by PARTFUN1:def 2;
hence R is total by ORDERS_2:def 1; :: thesis: verum