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