A1: {} in {{} } by TARSKI:def 1;
[{} ,{} ] in [:{{} },{{} }:] by ZFMISC_1:34;
hence op2 . {} ,{} = {} by CARD_1:87, FUNCT_2:65; :: thesis: ( op1 . {} = {} & op0 = {} )
thus op1 . {} = {} by A1, CARD_1:87, FUNCT_2:65; :: thesis: op0 = {}
thus op0 = {} ; :: thesis: verum