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 )
proof
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;
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 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