op1 c= [:{{} },{{} }:] by CARD_1:87;
then A1: op1 c= {[{} ,{} ]} by ZFMISC_1:35;
A2: {{} } = dom op1 by CARD_1:87, FUNCT_2:def 1;
rng op1 = {(op1 . {} )} by CARD_1:87, FUNCT_2:62;
then A3: op1 . {} = {} by CARD_1:87, ZFMISC_1:24;
{} in dom op1 by A2, TARSKI:def 1;
then [{} ,(op1 . {} )] in op1 by FUNCT_1:def 4;
then {[{} ,(op1 . {} )]} c= op1 by ZFMISC_1:37;
hence op1 = {[{} ,{} ]} by A1, A3, XBOOLE_0:def 10; :: thesis: verum