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