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