QC-WFF A is A -closed by Def11;
hence ex b₁ being set st
( b₁ is A -closed & not b₁ is empty ) ; :: thesis: verum