consider U1 being SubAlgebra of U0 such that
A1: U1 = u ;
reconsider A = the carrier of U1 as Subset of U0 by UNIALG_2:def 7;
take A ; :: thesis: ex U1 being SubAlgebra of U0 st
( u = U1 & A = the carrier of U1 )
take U1 ; :: thesis: ( u = U1 & A = the carrier of U1 )
thus ( u = U1 & A = the carrier of U1 ) by A1; :: thesis: verum