reconsider X = { (GenMSAlg (@ A)) where A is Element of SubSort U0 : verum } as set ;
take X ; :: thesis: for x being set holds
( x in X iff x is strict MSSubAlgebra of U0 )
let x be set ; :: thesis: ( x in X iff x is strict MSSubAlgebra of U0 )
thus ( x in X implies x is strict MSSubAlgebra of U0 ) :: thesis: ( x is strict MSSubAlgebra of U0 implies x in X )

proof

assume x in X ; :: thesis: x is strict MSSubAlgebra of U0
then consider A being Element of SubSort U0 such that
A1: x = GenMSAlg (@ A) ;
thus x is strict MSSubAlgebra of U0 by A1; :: thesis: verum

end;

assume x is strict MSSubAlgebra of U0 ; :: thesis: x in X
then reconsider a = x as strict MSSubAlgebra of U0 ;
reconsider A = the Sorts of a as MSSubset of U0 by Def10;
A is opers_closed by Def10;
then reconsider h = A as Element of SubSort U0 by Th15;
a = GenMSAlg (@ h) by Th23;
hence x in X ; :: thesis: verum