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