set C = bool the carrier of U0;
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 ) );
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 XBOOLE_0:sch 1();
 set P = meet X;
A3: the carrier of U0 in bool the carrier of U0 by ZFMISC_1:def 1;
for B being non empty Subset of U0 st B = the carrier of U0 holds
B is opers_closed by Th7;
then A4: the carrier of U0 in X by A2, A3;
A5: meet X c= the carrier of U0
proof
let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in meet X or t in the carrier of U0 )
assume t in meet X ; :: thesis: t in the carrier of U0
hence t in the carrier of U0 by A4, SETFAM_1:def 1; :: thesis: verum
end;
now
let x be set ; :: thesis: ( x in X implies A \/ (Constants U0) c= x )
assume x in X ; :: thesis: A \/ (Constants U0) c= x
then ( A c= x & Constants U0 c= x ) by A2;
hence A \/ (Constants U0) c= x by XBOOLE_1:8; :: thesis: verum
end;
then A6: A \/ (Constants U0) c= meet X by A4, SETFAM_1:6;
then reconsider P = meet X as non empty Subset of U0 by A1, A5;
A7: P is opers_closed
proof
let o be operation of U0; :: according to UNIALG_2:def 5 :: thesis: P is_closed_on o
let s be FinSequence of P; :: according to UNIALG_2:def 4 :: thesis: ( len s = arity o implies o . s in P )
assume A8: len s = arity o ; :: thesis: o . s in P
now
let a be set ; :: thesis: ( a in X implies o . s in a )
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;
a0 is opers_closed by A2, A9;
then A10: a0 is_closed_on o by Def5;
( P c= a0 & rng s c= P ) by A9, FINSEQ_1:def 4, SETFAM_1:4;
then rng s c= a0 by XBOOLE_1:1;
then reconsider s0 = s as FinSequence of a0 by FINSEQ_1:def 4;
o . s0 in a0 by A8, A10, Def4;
hence o . s in a ; :: thesis: verum
end;
hence o . s in P by A4, SETFAM_1:def 1; :: thesis: verum
end;
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 ) )
A11: E = UAStr(# P,(Opers U0,P) #) by A7, Def9;
A c= A \/ (Constants U0) by XBOOLE_1:7;
hence A c= the carrier of E by A6, A11, XBOOLE_1:1; :: 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 A12: A c= the carrier of U1 ; :: thesis: E is SubAlgebra of U1
set u1 = the carrier of U1;
A13: Constants U0 c= the carrier of U1
proof
let x be set ; :: 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
A14: ( a = x & 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 & a in rng o0 ) by A14;
consider n being Nat such that
A16: ( n in dom the charact of U0 & the charact of U0 . n = o0 ) by FINSEQ_2:11;
reconsider B = the carrier of U1 as non empty Subset of U0 by Def8;
A17: ( the charact of U1 = Opers U0,B & B is opers_closed ) by Def8;
A18: n in dom the charact of U1 by A16, Th10;
then reconsider o1 = the charact of U1 . n as operation of U1 by FUNCT_1:def 5;
A19: o1 = o0 /. B by A16, A17, A18, Def7;
consider y being set such that
A20: ( y in dom o0 & a = o0 . y ) by A15, FUNCT_1:def 5;
A21: B is_closed_on o0 by A17, Def5;
dom o0 = 0 -tuples_on the carrier of U0 by A15, Th2
.= {(<*> the carrier of U0)} by FINSEQ_2:112 ;
then y in {(<*> B)} by A20;
then y in 0 -tuples_on B by FINSEQ_2:112;
then y in (dom o0) /\ ((arity o0) -tuples_on B) by A15, A20, XBOOLE_0:def 4;
then A22: y in dom (o0 | ((arity o0) -tuples_on B)) by FUNCT_1:68;
then A23: y in dom (o0 /. B) by A21, Def6;
A24: o1 . y = (o0 | ((arity o0) -tuples_on B)) . y by A19, A21, Def6
.= a by A20, A22, FUNCT_1:68 ;
( o1 . y in rng o1 & rng o1 c= the carrier of U1 ) by A19, A23, FUNCT_1:def 5, RELSET_1:12;
hence x in the carrier of U1 by A14, A24; :: 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
( the charact of U1 = Opers U0,B & B is opers_closed ) ) ) by Def8;
then ( the carrier of U1 in bool the carrier of U0 & ( for B being non empty Subset of U0 st B = the carrier of U1 holds
B is opers_closed ) ) ;
then A25: the carrier of U1 in X by A2, A12, A13;
then A26: P c= the carrier of U1 by SETFAM_1:4;
thus the carrier of E is Subset of U1 by A11, A25, SETFAM_1:4; :: according to UNIALG_2:def 8 :: 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 A27: 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 Def8;
A28: ( the charact of U1 = Opers U0,u11 & u11 is opers_closed ) by Def8;
A29: ( dom the charact of U0 = dom (Opers U0,P) & dom the charact of U0 = dom (Opers U0,u11) ) by Def7;
A30: now
let o1 be operation of U1; :: thesis: B is_closed_on o1
consider n being Nat such that
A31: ( n in dom the charact of U1 & o1 = the charact of U1 . n ) by FINSEQ_2:11;
reconsider o0 = the charact of U0 . n as operation of U0 by A28, A29, A31, FUNCT_1:def 5;
A32: arity o0 = arity o1 by A31, Th9;
A33: u11 is_closed_on o0 by A28, Def5;
now
let s be FinSequence of B; :: thesis: ( len s = arity o1 implies o1 . s in B )
assume A34: len s = arity o1 ; :: thesis: o1 . s in B
reconsider sE = s as Element of P * by A11, A27, FINSEQ_1:def 11;
s is FinSequence of u11 by FINSEQ_2:27;
then reconsider s1 = s as Element of u11 * by FINSEQ_1:def 11;
A35: dom (o0 | ((arity o0) -tuples_on u11)) = (dom o0) /\ ((arity o0) -tuples_on u11) by FUNCT_1:68
.= ((arity o0) -tuples_on the carrier of U0) /\ ((arity o0) -tuples_on u11) by Th2
.= (arity o0) -tuples_on u11 by Th1 ;
s1 in { q where q is Element of u11 * : len q = arity o0 } by A32, A34;
then A36: s1 in dom (o0 | ((arity o0) -tuples_on u11)) by A35, FINSEQ_2:def 4;
A37: P is_closed_on o0 by A7, Def5;
o1 . s = (o0 /. u11) . s1 by A28, A31, Def7
.= (o0 | ((arity o0) -tuples_on u11)) . s1 by A33, Def6
.= o0 . sE by A36, FUNCT_1:68 ;
hence o1 . s in B by A11, A27, A32, A34, A37, Def4; :: thesis: verum
end;
hence B is_closed_on o1 by Def4; :: thesis: verum
end;
A38: dom (Opers U1,B) = dom the charact of U1 by Def7;
now
let n be Nat; :: thesis: ( n in dom the charact of U0 implies the charact of E . n = (Opers U1,B) . n )
assume A39: 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 5;
reconsider o1 = the charact of U1 . n as operation of U1 by A28, A29, A39, FUNCT_1:def 5;
A40: u11 is_closed_on o0 by A28, Def5;
A41: P is_closed_on o0 by A7, Def5;
thus the charact of E . n = o0 /. P by A11, A29, A39, Def7
.= o0 | ((arity o0) -tuples_on P) by A41, Def6
.= o0 | (((arity o0) -tuples_on u11) /\ ((arity o0) -tuples_on P)) by A26, Th1
.= (o0 | ((arity o0) -tuples_on u11)) | ((arity o0) -tuples_on P) by RELAT_1:100
.= (o0 /. u11) | ((arity o0) -tuples_on P) by A40, Def6
.= o1 | ((arity o0) -tuples_on P) by A28, A29, A39, Def7
.= o1 | ((arity o1) -tuples_on B) by A11, A27, A28, A29, A39, Th9
.= o1 /. B by A30, Def6
.= (Opers U1,B) . n by A28, A29, A38, A39, Def7 ; :: thesis: verum
end;
hence ( the charact of E = Opers U1,B & B is opers_closed ) by A11, A28, A29, A30, A38, Def5, FINSEQ_1:17; :: thesis: verum