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

proof

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in dom R )
assume x in S ; :: thesis: x in dom R
then ex y being set st
( y in S & [x,y] in R ) by A1;
hence x in dom R by RELAT_1:def 4; :: thesis: verum

end;

dom R c= S by RELAT_1:def 18;
then dom R = S by A2, XBOOLE_0:def 10;
hence R is total by PARTFUN1:def 2; :: 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 ) ) implies R is total ) ; :: thesis: verum