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

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