defpred S₁[ 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 (UnSubAlLattice U01) holds
ex u2 being object st
( u2 in the carrier of (UnSubAlLattice U02) & S₁[u1,u2] )

let u1 be object ; :: thesis:
assume u1 in the carrier of (UnSubAlLattice U01) ; :: thesis:
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 (UnSubAlLattice U02) by UNIALG_2:def 14;
take u2 ; :: thesis:
thus ( u2 in the carrier of (UnSubAlLattice U02) & S₁[u1,u2] ) by A2; :: thesis:

end;

consider f1 being Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02) such that
A3: for u1 being object st u1 in the carrier of (UnSubAlLattice U01) holds
S₁[u1,f1 . u1] from FUNCT_2:sch 1(A1);
take f1 ; :: thesis:
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:

end;