let A be set ; :: thesis: {A} c= bool A
A in bool A by Def1;
hence {A} c= bool A by Lm1; :: thesis: verum