take X ; :: thesis: ( X is SubAlgebra of X & not X is proper )
X is SubAlgebra of X by Th22;
hence ( X is SubAlgebra of X & not X is proper ) by Def13; :: thesis: verum