ex H being strict Subgroup of F₁() st the carrier of H = meet { A where A is Subset of F₁() : ex K being strict Subgroup of F₁() st
( A = the carrier of K & P₁[K] ) }

A1: ex H being strict Subgroup of F₁() st P₁[H]