let R be Relation; :: thesis: R " {} = {}
set x = the Element of R " {};
( the Element of R " {} in R " {} iff ex y being set st
( [ the Element of R " {},y] in R & y in {} ) ) by Def14;
hence R " {} = {} ; :: thesis: verum