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 )

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

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 is strict SubAlgebra of U0
; :: thesis: x in X
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;then ex A being Subset of U0 st

( x = GenUnivAlg A & not A is empty ) ;

hence x is strict SubAlgebra of U0 ; :: thesis: verum

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