let Y be non empty set ; :: thesis: ERl (%O Y) = nabla Y
nabla Y c= ERl (%O Y)

proof

let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in nabla Y or [x1,x2] in ERl (%O Y) )
assume A1: [x1,x2] in nabla Y ; :: thesis: [x1,x2] in ERl (%O Y)
A2: Y in %O Y by TARSKI:def 1;
( x1 in Y & x2 in Y ) by A1, ZFMISC_1:87;
hence [x1,x2] in ERl (%O Y) by A2, Def6; :: thesis: verum

end;

hence ERl (%O Y) = nabla Y ; :: thesis: verum