let W1, W2 be strict OSSubAlgebra of OU0; :: thesis: ( A is OSSubset of W1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
W1 is OSSubAlgebra of OU1 ) & A is OSSubset of W2 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
W2 is OSSubAlgebra of OU1 ) implies W1 = W2 )
assume ( A is OSSubset of W1 & ( for U1 being OSSubAlgebra of OU0 st A is OSSubset of U1 holds
W1 is OSSubAlgebra of U1 ) & A is OSSubset of W2 & ( for U2 being OSSubAlgebra of OU0 st A is OSSubset of U2 holds
W2 is OSSubAlgebra of U2 ) ) ; :: thesis: W1 = W2
then ( W1 is strict OSSubAlgebra of W2 & W2 is strict OSSubAlgebra of W1 ) ;
hence W1 = W2 by MSUALG_2:7; :: thesis: verum