reconsider f = (x,y) --> (({} UN),{({} UN)}) as Function ;
f c= [:{x,y},{({} UN),{({} UN)}}:] by Lm1;
hence (x,y) --> (({} UN),{({} UN)}) is Element of UN by Th13; :: thesis: verum