reconsider H1 = meet ((Carr U0) .: H) as non empty Subset of U0 by Th12;
UniAlgSetClosed H1 = UAStr(# H1,(Opers (U0,H1)) #) by Th14, UNIALG_2:def 8;
hence ex b₁ being strict SubAlgebra of U0 st the carrier of b₁ = meet ((Carr U0) .: H) ; :: thesis: verum