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

proof

let x1, x2 be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in nabla Y or [x1,x2] in ERl (%O Y) )
assume A2: [x1,x2] in nabla Y ; :: thesis: [x1,x2] in ERl (%O Y)
A3: Y in %O Y by TARSKI:def 1;
A4: ( x1 in Y & x2 in Y ) by A2, ZFMISC_1:106;
thus [x1,x2] in ERl (%O Y) by A3, A4, Def6; :: thesis: verum

end;

thus ERl (%O Y) = nabla Y by A1, XBOOLE_0:def 10; :: thesis: verum