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