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 )
thus A2: [:{{} },{{} }:] in UN by A1, CLASSES2:67; :: thesis: ( op2 in UN & op1 in UN )
A3: Funcs {{} },{{} } in UN by A1, CLASSES2:67;
A4: Funcs [:{{} },{{} }:],{{} } in UN by A1, A2, CLASSES2:67;
op2 in Funcs [:{{} },{{} }:],{{} } by CARD_1:87, FUNCT_2:11;
hence op2 in UN by A4, Th4; :: thesis: op1 in UN
op1 in Funcs {{} },{{} } by CARD_1:87, FUNCT_2:11;
hence op1 in UN by A3, Th4; :: thesis: verum