set p = the Point of T;
Cl { the Point of T} is irreducible by Th17;
hence ex b₁ being Subset of T st b₁ is irreducible ; :: thesis: verum