defpred S1[ set ] means ( A c= \$1 & Constants U0 c= \$1 & ( for B being non empty Subset of U0 st B = \$1 holds
B is opers_closed ) );
set C = bool the carrier of U0;
consider X being set such that
A2: for x being set holds
( x in X iff ( x in bool the carrier of U0 & S1[x] ) ) from set P = meet X;
( the carrier of U0 in bool the carrier of U0 & ( for B being non empty Subset of U0 st B = the carrier of U0 holds
B is opers_closed ) ) by ;
then A3: the carrier of U0 in X by A2;
A4: meet X c= the carrier of U0 by ;
now :: thesis: for x being set st x in X holds
A \/ () c= x
let x be set ; :: thesis: ( x in X implies A \/ () c= x )
assume x in X ; :: thesis: A \/ () c= x
then ( A c= x & Constants U0 c= x ) by A2;
hence A \/ () c= x by XBOOLE_1:8; :: thesis: verum
end;
then A5: A \/ () c= meet X by ;
then reconsider P = meet X as non empty Subset of U0 by A1, A4;
take E = UniAlgSetClosed P; :: thesis: ( A c= the carrier of E & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
E is SubAlgebra of U1 ) )

A6: P is opers_closed
proof
let o be operation of U0; :: according to UNIALG_2:def 4 :: thesis:
let s be FinSequence of P; :: according to UNIALG_2:def 3 :: thesis: ( len s = arity o implies o . s in P )
assume A7: len s = arity o ; :: thesis: o . s in P
now :: thesis: for a being set st a in X holds
o . s in a
let a be set ; :: thesis: ( a in X implies o . s in a )
A8: rng s c= P by FINSEQ_1:def 4;
assume A9: a in X ; :: thesis: o . s in a
then reconsider a0 = a as Subset of U0 by A2;
( A c= a0 & Constants U0 c= a0 ) by A2, A9;
then reconsider a0 = a0 as non empty Subset of U0 by A1;
P c= a0 by ;
then rng s c= a0 by A8;
then reconsider s0 = s as FinSequence of a0 by FINSEQ_1:def 4;
a0 is opers_closed by A2, A9;
then a0 is_closed_on o ;
then o . s0 in a0 by A7;
hence o . s in a ; :: thesis: verum
end;
hence o . s in P by ; :: thesis: verum
end;
then A10: E = UAStr(# P,(Opers (U0,P)) #) by Def8;
A c= A \/ () by XBOOLE_1:7;
hence A c= the carrier of E by ; :: thesis: for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
E is SubAlgebra of U1

let U1 be SubAlgebra of U0; :: thesis: ( A c= the carrier of U1 implies E is SubAlgebra of U1 )
assume A11: A c= the carrier of U1 ; :: thesis: E is SubAlgebra of U1
set u1 = the carrier of U1;
A12: Constants U0 c= the carrier of U1
proof
reconsider B = the carrier of U1 as non empty Subset of U0 by Def7;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Constants U0 or x in the carrier of U1 )
assume x in Constants U0 ; :: thesis: x in the carrier of U1
then consider a being Element of U0 such that
A13: a = x and
A14: ex o being operation of U0 st
( arity o = 0 & a in rng o ) ;
consider o0 being operation of U0 such that
A15: arity o0 = 0 and
A16: a in rng o0 by A14;
consider y being object such that
A17: y in dom o0 and
A18: a = o0 . y by ;
dom o0 = 0 -tuples_on the carrier of U0 by
.= {(<*> the carrier of U0)} by FINSEQ_2:94 ;
then y in {(<*> B)} by A17;
then y in 0 -tuples_on B by FINSEQ_2:94;
then y in (dom o0) /\ ((arity o0) -tuples_on B) by ;
then A19: y in dom (o0 | ((arity o0) -tuples_on B)) by RELAT_1:61;
consider n being Nat such that
A20: n in dom the charact of U0 and
A21: the charact of U0 . n = o0 by FINSEQ_2:10;
A22: n in dom the charact of U1 by ;
then reconsider o1 = the charact of U1 . n as operation of U1 by FUNCT_1:def 3;
the charact of U1 = Opers (U0,B) by Def7;
then A23: o1 = o0 /. B by ;
B is opers_closed by Def7;
then A24: B is_closed_on o0 ;
then y in dom (o0 /. B) by ;
then A25: o1 . y in rng o1 by ;
A26: rng o1 c= the carrier of U1 by RELAT_1:def 19;
o1 . y = (o0 | ((arity o0) -tuples_on B)) . y by
.= a by ;
hence x in the carrier of U1 by ; :: thesis: verum
end;
( the carrier of U1 is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of U1 holds
B is opers_closed ) ) by Def7;
then A27: the carrier of U1 in X by A2, A11, A12;
hence the carrier of E is Subset of U1 by ; :: according to UNIALG_2:def 7 :: thesis: for B being non empty Subset of U1 st B = the carrier of E holds
( the charact of E = Opers (U1,B) & B is opers_closed )

let B be non empty Subset of U1; :: thesis: ( B = the carrier of E implies ( the charact of E = Opers (U1,B) & B is opers_closed ) )
assume A28: B = the carrier of E ; :: thesis: ( the charact of E = Opers (U1,B) & B is opers_closed )
reconsider u11 = the carrier of U1 as non empty Subset of U0 by Def7;
A29: the charact of U1 = Opers (U0,u11) by Def7;
A30: dom the charact of U0 = dom (Opers (U0,u11)) by Def6;
A31: u11 is opers_closed by Def7;
A32: now :: thesis: for o1 being operation of U1 holds B is_closed_on o1
let o1 be operation of U1; :: thesis: B is_closed_on o1
consider n being Nat such that
A33: n in dom the charact of U1 and
A34: o1 = the charact of U1 . n by FINSEQ_2:10;
reconsider o0 = the charact of U0 . n as operation of U0 by ;
A35: arity o0 = arity o1 by ;
A36: u11 is_closed_on o0 by A31;
now :: thesis: for s being FinSequence of B st len s = arity o1 holds
o1 . s in B
let s be FinSequence of B; :: thesis: ( len s = arity o1 implies o1 . s in B )
A37: P is_closed_on o0 by A6;
reconsider sE = s as Element of P * by ;
s is FinSequence of u11 by FINSEQ_2:24;
then reconsider s1 = s as Element of u11 * by FINSEQ_1:def 11;
A38: dom (o0 | ((arity o0) -tuples_on u11)) = (dom o0) /\ ((arity o0) -tuples_on u11) by RELAT_1:61
.= ((arity o0) -tuples_on the carrier of U0) /\ ((arity o0) -tuples_on u11) by MARGREL1:22
.= (arity o0) -tuples_on u11 by MARGREL1:21 ;
assume A39: len s = arity o1 ; :: thesis: o1 . s in B
then s1 in { q where q is Element of u11 * : len q = arity o0 } by A35;
then A40: s1 in dom (o0 | ((arity o0) -tuples_on u11)) by ;
o1 . s = (o0 /. u11) . s1 by
.= (o0 | ((arity o0) -tuples_on u11)) . s1 by
.= o0 . sE by ;
hence o1 . s in B by A10, A28, A35, A39, A37; :: thesis: verum
end;
hence B is_closed_on o1 ; :: thesis: verum
end;
A41: dom (Opers (U1,B)) = dom the charact of U1 by Def6;
A42: dom the charact of U0 = dom (Opers (U0,P)) by Def6;
A43: P c= the carrier of U1 by ;
now :: thesis: for n being Nat st n in dom the charact of U0 holds
the charact of E . n = (Opers (U1,B)) . n
let n be Nat; :: thesis: ( n in dom the charact of U0 implies the charact of E . n = (Opers (U1,B)) . n )
assume A44: n in dom the charact of U0 ; :: thesis: the charact of E . n = (Opers (U1,B)) . n
then reconsider o0 = the charact of U0 . n as operation of U0 by FUNCT_1:def 3;
reconsider o1 = the charact of U1 . n as operation of U1 by ;
A45: u11 is_closed_on o0 by A31;
A46: P is_closed_on o0 by A6;
thus the charact of E . n = o0 /. P by
.= o0 | ((arity o0) -tuples_on P) by
.= o0 | (((arity o0) -tuples_on u11) /\ ((arity o0) -tuples_on P)) by
.= (o0 | ((arity o0) -tuples_on u11)) | ((arity o0) -tuples_on P) by RELAT_1:71
.= (o0 /. u11) | ((arity o0) -tuples_on P) by
.= o1 | ((arity o0) -tuples_on P) by
.= o1 | ((arity o1) -tuples_on B) by A10, A28, A29, A30, A44, Th6
.= o1 /. B by
.= (Opers (U1,B)) . n by A29, A30, A41, A44, Def6 ; :: thesis: verum
end;
hence ( the charact of E = Opers (U1,B) & B is opers_closed ) by ; :: thesis: verum