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