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

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