let W1, W2 be strict SubAlgebra of U0; :: thesis: ( A c= the carrier of W1 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
W1 is SubAlgebra of U1 ) & A c= the carrier of W2 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
W2 is SubAlgebra of U1 ) implies W1 = W2 )
assume ( A c= the carrier of W1 & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
W1 is SubAlgebra of U1 ) & A c= the carrier of W2 & ( for U2 being SubAlgebra of U0 st A c= the carrier of U2 holds
W2 is SubAlgebra of U2 ) ) ; :: thesis: W1 = W2
then ( W1 is strict SubAlgebra of W2 & W2 is strict SubAlgebra of W1 ) ;
hence W1 = W2 by Th10; :: thesis: verum