defpred S1[ object , object ] means for U1 being strict SubAlgebra of U01 st U1 = \$1 holds
for S being Subset of U02 st S = F .: the carrier of U1 holds
\$2 = GenUnivAlg (F .: the carrier of U1);
A1: for u1 being object st u1 in the carrier of () holds
ex u2 being object st
( u2 in the carrier of () & S1[u1,u2] )
proof
let u1 be object ; :: thesis: ( u1 in the carrier of () implies ex u2 being object st
( u2 in the carrier of () & S1[u1,u2] ) )

assume u1 in the carrier of () ; :: thesis: ex u2 being object st
( u2 in the carrier of () & S1[u1,u2] )

then consider U2 being strict SubAlgebra of U01 such that
A2: U2 = u1 by Th1;
reconsider u2 = GenUnivAlg (F .: the carrier of U2) as strict SubAlgebra of U02 ;
reconsider u2 = u2 as Element of () by UNIALG_2:def 14;
take u2 ; :: thesis: ( u2 in the carrier of () & S1[u1,u2] )
thus ( u2 in the carrier of () & S1[u1,u2] ) by A2; :: thesis: verum
end;
consider f1 being Function of the carrier of (), the carrier of () such that
A3: for u1 being object st u1 in the carrier of () holds
S1[u1,f1 . u1] from take f1 ; :: thesis: for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
f1 . U1 = GenUnivAlg H

thus for U1 being strict SubAlgebra of U01
for H being Subset of U02 st H = F .: the carrier of U1 holds
f1 . U1 = GenUnivAlg H :: thesis: verum
proof
let U1 be strict SubAlgebra of U01; :: thesis: for H being Subset of U02 st H = F .: the carrier of U1 holds
f1 . U1 = GenUnivAlg H

let S be Subset of U02; :: thesis: ( S = F .: the carrier of U1 implies f1 . U1 = GenUnivAlg S )
A4: U1 is Element of Sub U01 by UNIALG_2:def 14;
assume S = F .: the carrier of U1 ; :: thesis: f1 . U1 = GenUnivAlg S
hence f1 . U1 = GenUnivAlg S by A3, A4; :: thesis: verum
end;