defpred S_{1}[ 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_{1}[u1,u2] )

A3: for u1 being object st u1 in the carrier of (UnSubAlLattice U01) holds

S_{1}[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

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

proof

consider f1 being Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02) such that
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_{1}[u1,u2] ) )

assume u1 in the carrier of (UnSubAlLattice U01) ; :: thesis: ex u2 being object st

( u2 in the carrier of (UnSubAlLattice U02) & S_{1}[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_{1}[u1,u2] )

thus ( u2 in the carrier of (UnSubAlLattice U02) & S_{1}[u1,u2] )
by A2; :: thesis: verum

end;( u2 in the carrier of (UnSubAlLattice U02) & S

assume u1 in the carrier of (UnSubAlLattice U01) ; :: thesis: ex u2 being object st

( u2 in the carrier of (UnSubAlLattice U02) & S

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

thus ( u2 in the carrier of (UnSubAlLattice U02) & S

A3: for u1 being object st u1 in the carrier of (UnSubAlLattice U01) holds

S

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