scheme :: GROUP_22:sch 1
CharMeet{ F₁() -> Group, P₁[ set ] } :

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

provided

A1: for phi being Automorphism of F₁()
for H being strict Subgroup of F₁() st P₁[H] holds
P₁[ Image (phi | H)] and
A2: ex H being strict Subgroup of F₁() st P₁[H]