theorem Th20: :: BVFUNC_1:21

for Y being non empty set
for a being constant Function of Y,BOOLEAN holds
( a = O_el Y or a = I_el Y )