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: dom R c= S by RELAT_1:def 18;
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 consider y being set such that
y in S and
A3: [x,y] in R by A1;
thus x in dom R by A3, RELAT_1:def 4; :: thesis: verum

end;

then dom R = S by A2, XBOOLE_0:def 10;
hence R is total by PARTFUN1:def 4; :: 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