let S be OrderSortedSign; :: thesis: for U0 being strict non-empty OSAlgebra of S
for A being MSSubset of U0 holds
( A is OSGeneratorSet of U0 iff for O being OSSubset of U0 st O = OSCl A holds
GenOSAlg O = U0 )
let U0 be strict non-empty OSAlgebra of S; :: thesis: for A being MSSubset of U0 holds
( A is OSGeneratorSet of U0 iff for O being OSSubset of U0 st O = OSCl A holds
GenOSAlg O = U0 )
let A be MSSubset of U0; :: thesis: ( A is OSGeneratorSet of U0 iff for O being OSSubset of U0 st O = OSCl A holds
GenOSAlg O = U0 )
thus ( A is OSGeneratorSet of U0 implies for O being OSSubset of U0 st O = OSCl A holds
GenOSAlg O = U0 ) :: thesis: ( ( for O being OSSubset of U0 st O = OSCl A holds
GenOSAlg O = U0 ) implies A is OSGeneratorSet of U0 )
proof
reconsider U1 = U0 as MSSubAlgebra of U0 by MSUALG_2:5;
assume A1: A is OSGeneratorSet of U0 ; :: thesis: for O being OSSubset of U0 st O = OSCl A holds
GenOSAlg O = U0
let O be OSSubset of U0; :: thesis: ( O = OSCl A implies GenOSAlg O = U0 )
assume O = OSCl A ; :: thesis: GenOSAlg O = U0
then the Sorts of (GenOSAlg O) = the Sorts of U1 by A1, Def1;
hence GenOSAlg O = U0 by MSUALG_2:9; :: thesis: verum
end;
assume A2: for O being OSSubset of U0 st O = OSCl A holds
GenOSAlg O = U0 ; :: thesis: A is OSGeneratorSet of U0
let O be OSSubset of U0; :: according to OSAFREE:def 1 :: thesis: ( O = OSCl A implies the Sorts of (GenOSAlg O) = the Sorts of U0 )
assume O = OSCl A ; :: thesis: the Sorts of (GenOSAlg O) = the Sorts of U0
hence the Sorts of (GenOSAlg O) = the Sorts of U0 by A2; :: thesis: verum