let R be RelStr ; :: thesis: ( the InternalRel of R is_reflexive_in the carrier of R implies R is serial )
assume A1: the InternalRel of R is_reflexive_in the carrier of R ; :: thesis: R is serial
set IR = the InternalRel of R;
set X = the carrier of R;
for x being object st x in the carrier of R holds
ex y being object st
( y in the carrier of R & [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
( y in the carrier of R & [x,y] in the InternalRel of R ) )
assume A2: 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 [x,x] in the InternalRel of R by A1, RELAT_2:def 1;
hence ex y being object st
( y in the carrier of R & [x,y] in the InternalRel of R ) by A2; :: thesis: verum
end;
hence R is serial by Def1; :: thesis: verum