let UN be Universe; :: thesis: ( {{} } in UN & [{{} },{{} }] in UN & [:{{} },{{} }:] in UN & op2 in UN & op1 in UN )
set D = {{} };
thus A1: {{} } in UN by CLASSES2:62, CLASSES2:63; :: thesis: ( [{{} },{{} }] in UN & [:{{} },{{} }:] in UN & op2 in UN & op1 in UN )
hence [{{} },{{} }] in UN by CLASSES2:64; :: thesis: ( [:{{} },{{} }:] in UN & op2 in UN & op1 in UN )
A2: op2 in Funcs [:{{} },{{} }:],{{} } by CARD_1:87, FUNCT_2:11;
thus [:{{} },{{} }:] in UN by A1, CLASSES2:67; :: thesis: ( op2 in UN & op1 in UN )
then Funcs [:{{} },{{} }:],{{} } in UN by A1, CLASSES2:67;
hence op2 in UN by A2, ORDINAL1:19; :: thesis: op1 in UN
A3: op1 in Funcs {{} },{{} } by CARD_1:87, FUNCT_2:11;
Funcs {{} },{{} } in UN by A1, CLASSES2:67;
hence op1 in UN by A3, ORDINAL1:19; :: thesis: verum