let W1, W2 be strict MSSubAlgebra of U0; :: thesis: ( A is MSSubset of W1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
W1 is MSSubAlgebra of U1 ) & A is MSSubset of W2 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
W2 is MSSubAlgebra of U1 ) implies W1 = W2 )
assume ( A is MSSubset of W1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
W1 is MSSubAlgebra of U1 ) & A is MSSubset of W2 & ( for U2 being MSSubAlgebra of U0 st A is MSSubset of U2 holds
W2 is MSSubAlgebra of U2 ) ) ; :: thesis: W1 = W2
then ( W1 is strict MSSubAlgebra of W2 & W2 is strict MSSubAlgebra of W1 ) ;
hence W1 = W2 by Th7; :: thesis: verum