let Y be set ; :: thesis: for R being Relation st Y <> {} & Y c= rng R holds
R " Y <> {}
let R be Relation; :: thesis: ( Y <> {} & Y c= rng R implies R " Y <> {} )
assume that
A1: Y <> {} and
A2: Y c= rng R ; :: thesis: R " Y <> {}
set y = the Element of Y;
A3: the Element of Y in rng R by A1, A2;
then ex x being object st [x, the Element of Y] in R by XTUPLE_0:def 13;
hence R " Y <> {} by A1, A3, Th123; :: thesis: verum