let Y be non empty set ; :: thesis: for R being Relation of Y holds R c= nabla Y
let R be Relation of Y; :: thesis: R c= nabla Y
nabla Y = [:Y,Y:] by EQREL_1:def 1;
hence R c= nabla Y ; :: thesis: verum