set X = { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ;
take { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ; :: thesis: for x being object holds
( x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } iff x is strict OSSubAlgebra of OU0 )
let x be object ; :: thesis: ( x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } iff x is strict OSSubAlgebra of OU0 )
thus ( x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } implies x is strict OSSubAlgebra of OU0 ) :: thesis: ( x is strict OSSubAlgebra of OU0 implies x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } )

proof

assume x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ; :: thesis: x is strict OSSubAlgebra of OU0
then ex A being Element of OSSubSort OU0 st x = GenOSAlg (@ A) ;
hence x is strict OSSubAlgebra of OU0 ; :: thesis: verum

end;

assume x is strict OSSubAlgebra of OU0 ; :: thesis: x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum }
then reconsider a = x as strict OSSubAlgebra of OU0 ;
reconsider A = the Sorts of a as OSSubset of OU0 by Th5;
A is opers_closed by Th5;
then reconsider h = A as Element of OSSubSort OU0 by Th20;
a = GenOSAlg (@ h) by Th35;
hence x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ; :: thesis: verum