{(VERUM Al)} is Consistent by HENMODEL:13;
hence ex b₁ being Subset of (CQC-WFF Al) st
( not b₁ is empty & b₁ is Consistent ) ; :: thesis: verum