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