A1: for B being strict non-empty finitely-generated MSSubAlgebra of F₂() holds P₁[B] and
A2: for A, B being non-empty MSAlgebra over F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] and
A3: for A being non-empty MSAlgebra over F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B] and
A4: for A being non-empty MSAlgebra over F₁()
for R being MSCongruence of A st P₁[A] holds
P₁[ QuotMSAlg (A,R)] and
A5: for I being set
for F being MSAlgebra-Family of I,F₁() st ( for i being set st i in I holds
ex A being MSAlgebra over F₁() st
( A = F . i & P₁[A] ) ) holds
P₁[ product F]