reconsider X = { (GenUnivAlg A) where A is Subset of U0 : not A is empty } as set ;
take X ; :: thesis: for x being object holds
( x in X iff x is strict SubAlgebra of U0 )
let x be object ; :: thesis: ( x in X iff x is strict SubAlgebra of U0 )
thus ( x in X implies x is strict SubAlgebra of U0 ) :: thesis: ( x is strict SubAlgebra of U0 implies x in X )

proof

assume x in X ; :: thesis: x is strict SubAlgebra of U0
then ex A being Subset of U0 st
( x = GenUnivAlg A & not A is empty ) ;
hence x is strict SubAlgebra of U0 ; :: thesis: verum

end;

assume x is strict SubAlgebra of U0 ; :: thesis: x in X
then reconsider a = x as strict SubAlgebra of U0 ;
reconsider A = the carrier of a as non empty Subset of U0 by Def7;
a = GenUnivAlg A by Th19;
hence x in X ; :: thesis: verum