theorem :: MODELC_1:26

for S being non empty set
for R being Relation of S,S holds
( R is total iff for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R ) ) by Lm30, Lm31;