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

X is SubAlgebra of X by Th22;

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