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] )

proof

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

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: 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;