let U be Universe; :: thesis: 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
let X, Y, Z be set ; :: thesis: ( X in U & Y in U & Z in U implies bool [:[:(bool [:X,Y:]),(bool [:X,Y:]):],(bool [:Z,Y:]):] in U )
assume that
A1: X in U and
A2: Y in U and
A3: Z in U ; :: thesis: bool [:[:(bool [:X,Y:]),(bool [:X,Y:]):],(bool [:Z,Y:]):] in U
reconsider X = X, Y = Y, Z = Z as Element of U by A1, A2, A3;
bool [:[:(bool [:X,Y:]),(bool [:X,Y:]):],(bool [:Z,Y:]):] in U ;
hence bool [:[:(bool [:X,Y:]),(bool [:X,Y:]):],(bool [:Z,Y:]):] in U ; :: thesis: verum