let S be set ; :: thesis: for R being Relation of S,S st R is total holds
for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R )
let R be Relation of S,S; :: thesis: ( R is total implies for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R ) )
( R is total implies for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R ) )

proof

assume A1: R is total ; :: thesis: for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R )
for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R )

proof

let x be set ; :: thesis: ( x in S implies ex y being set st
( y in S & [x,y] in R ) )
assume A2: x in S ; :: thesis: ex y being set st
( y in S & [x,y] in R )
dom R = S by A1, PARTFUN1:def 2;
then consider y being Element of S such that
A3: [x,y] in R by A2, RELSET_1:24;
take y ; :: thesis: ( y in S & [x,y] in R )
thus ( y in S & [x,y] in R ) by A2, A3; :: thesis: verum

end;

hence for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R ) ; :: thesis: verum

end;

hence ( R is total implies for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R ) ) ; :: thesis: verum