set f = id (bool X);
reconsider f = id (bool X) as Function of (bool X),(bool X) ;
A1: f is idempotent ;
A2: f is extensive ;
{} c= X ;
then A3: f is empty-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 closure by A1, A2, A3; :: thesis: verum