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

nabla Y c= ERl (%O Y)

nabla Y c= ERl (%O Y)

proof

hence
ERl (%O Y) = nabla Y
; :: thesis: verum
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;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