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