let x be set ; :: thesis: for R being Relation st x in dom R holds
ex y being set st y in rng R
let R be Relation; :: thesis: ( x in dom R implies ex y being set st y in rng R )
assume x in dom R ; :: thesis: ex y being set st y in rng R
then consider y being set such that
A1: [x,y] in R by Def4;
take y ; :: thesis: y in rng R
thus y in rng R by A1, Def5; :: thesis: verum