reconsider X = { (GenMSAlg (@ A)) where A is Element of SubSort U0 : verum } as set ;

take X ; :: thesis: for x being object holds

( x in X iff x is strict MSSubAlgebra of U0 )

let x be object ; :: 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 )

then reconsider a = x as strict MSSubAlgebra of U0 ;

reconsider A = the Sorts of a as MSSubset of U0 by Def9;

A is opers_closed by Def9;

then reconsider h = A as Element of SubSort U0 by Th14;

a = GenMSAlg (@ h) by Th22;

hence x in X ; :: thesis: verum

take X ; :: thesis: for x being object holds

( x in X iff x is strict MSSubAlgebra of U0 )

let x be object ; :: 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 is strict MSSubAlgebra of U0
; :: thesis: x in X
assume
x in X
; :: thesis: x is strict MSSubAlgebra of U0

then ex A being Element of SubSort U0 st x = GenMSAlg (@ A) ;

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

end;then ex A being Element of SubSort U0 st x = GenMSAlg (@ A) ;

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

then reconsider a = x as strict MSSubAlgebra of U0 ;

reconsider A = the Sorts of a as MSSubset of U0 by Def9;

A is opers_closed by Def9;

then reconsider h = A as Element of SubSort U0 by Th14;

a = GenMSAlg (@ h) by Th22;

hence x in X ; :: thesis: verum