theorem :: CLASSES2:58

for x, y being set
for U being Universe st x in U & y in U holds
( {x,y} in U & [x,y] in U ) by Th2, Th3;