theorem Th31: :: CLASSES4:31

for UN being Universe
for u, v being Element of UN holds {[u,{}],[v,{{}}]} = [:{u},{{}}:] \/ [:{v},{{{}}}:]