let U1, U2 be non empty set ; :: thesis: for R being Relation of U1,U2 holds 0 -placesOf R = id {{}}
let R be Relation of U1,U2; :: thesis: 0 -placesOf R = id {{}}
(0 -placesOf R) \+\ (id {{}}) = {} ;
hence 0 -placesOf R = id {{}} by FOMODEL0:29; :: thesis: verum