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:56, CLASSES2:57; :: thesis: ( [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN )
hence [{{}},{{}}] in UN by CLASSES2:58; :: thesis: ( [:{{}},{{}}:] in UN & op2 in UN & op1 in UN )
A2: op2 in Funcs ([:{{}},{{}}:],{{}}) by FUNCT_2:8;
thus [:{{}},{{}}:] in UN by A1, CLASSES2:61; :: thesis: ( op2 in UN & op1 in UN )
then Funcs ([:{{}},{{}}:],{{}}) in UN by A1, CLASSES2:61;
hence op2 in UN by A2, ORDINAL1:10; :: thesis: op1 in UN
A3: op1 in Funcs ({{}},{{}}) by FUNCT_2:8;
Funcs ({{}},{{}}) in UN by A1, CLASSES2:61;
hence op1 in UN by A3, ORDINAL1:10; :: thesis: verum