set f = id (bool X);
reconsider f = id (bool X) as Function of (bool X),(bool X) ;
A1: f is idempotent ;
A2: f is intensive ;
X in bool X by ZFMISC_1:def 1;
then A3: f is universe-preserving by FUNCT_1:17;
f is /\-preserving ;
hence for b₁ being Function of (bool X),(bool X) st b₁ = id (bool X) holds
b₁ is interior by A1, A2, A3; :: thesis: verum