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, TARSKI:def 3;
then ex y being set st [ the Element of X,y] in R by Def4;
hence R .: X <> {} by A1, A3, Th143; :: thesis: verum