theorem :: CLASSES5:68

for U being Universe
for X, Y, Z being set st X in U & Y in U & Z in U holds
bool [:[:(bool [:X,Y:]),(bool [:X,Y:]):],(bool [:Z,Y:]):] in U