defpred S_{1}[ 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 & S_{1}[x] ) )
from XFAMILY:sch 1();

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 Th4, ZFMISC_1:def 1;

then A3: the carrier of U0 in X by A2;

A4: meet X c= the carrier of U0 by A3, SETFAM_1:def 1;

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

A c= A \/ (Constants U0) by XBOOLE_1:7;

hence A c= the carrier of E by A5, A10; :: 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

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 A10, SETFAM_1:3; :: 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;

A42: dom the charact of U0 = dom (Opers (U0,P)) by Def6;

A43: P c= the carrier of U1 by A27, SETFAM_1:3;

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 & S

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 Th4, ZFMISC_1:def 1;

then A3: the carrier of U0 in X by A2;

A4: meet X c= the carrier of U0 by A3, SETFAM_1:def 1;

now :: thesis: for x being set st x in X holds

A \/ (Constants U0) c= x

then A5:
A \/ (Constants U0) c= meet X
by A3, SETFAM_1:5;A \/ (Constants U0) c= x

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

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

then A10:
E = UAStr(# P,(Opers (U0,P)) #)
by Def8;
let o be operation of U0; :: according to UNIALG_2:def 4 :: thesis: P is_closed_on o

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

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

hence
o . s in P
by A3, SETFAM_1:def 1; :: thesis: verumo . 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 A9, SETFAM_1:3;

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;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 A9, SETFAM_1:3;

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

A c= A \/ (Constants U0) by XBOOLE_1:7;

hence A c= the carrier of E by A5, A10; :: 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

( the carrier of U1 is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of U1 holds
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 A16, FUNCT_1:def 3;

dom o0 = 0 -tuples_on the carrier of U0 by A15, MARGREL1:22

.= {(<*> 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 A15, A17, XBOOLE_0:def 4;

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 A20, Th7;

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 A21, A22, Def6;

B is opers_closed by Def7;

then A24: B is_closed_on o0 ;

then y in dom (o0 /. B) by A19, Def5;

then A25: o1 . y in rng o1 by A23, FUNCT_1:def 3;

A26: rng o1 c= the carrier of U1 by RELAT_1:def 19;

o1 . y = (o0 | ((arity o0) -tuples_on B)) . y by A23, A24, Def5

.= a by A18, A19, FUNCT_1:47 ;

hence x in the carrier of U1 by A13, A25, A26; :: thesis: verum

end;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 A16, FUNCT_1:def 3;

dom o0 = 0 -tuples_on the carrier of U0 by A15, MARGREL1:22

.= {(<*> 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 A15, A17, XBOOLE_0:def 4;

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 A20, Th7;

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 A21, A22, Def6;

B is opers_closed by Def7;

then A24: B is_closed_on o0 ;

then y in dom (o0 /. B) by A19, Def5;

then A25: o1 . y in rng o1 by A23, FUNCT_1:def 3;

A26: rng o1 c= the carrier of U1 by RELAT_1:def 19;

o1 . y = (o0 | ((arity o0) -tuples_on B)) . y by A23, A24, Def5

.= a by A18, A19, FUNCT_1:47 ;

hence x in the carrier of U1 by A13, A25, A26; :: thesis: verum

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 A10, SETFAM_1:3; :: 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

A41:
dom (Opers (U1,B)) = dom the charact of U1
by Def6;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 A29, A30, A33, FUNCT_1:def 3;

A35: arity o0 = arity o1 by A33, A34, Th6;

A36: u11 is_closed_on o0 by A31;

end;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 A29, A30, A33, FUNCT_1:def 3;

A35: arity o0 = arity o1 by A33, A34, Th6;

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

hence
B is_closed_on o1
; :: thesis: verumo1 . 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 A10, A28, FINSEQ_1:def 11;

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 A38, FINSEQ_2:def 4;

o1 . s = (o0 /. u11) . s1 by A29, A33, A34, Def6

.= (o0 | ((arity o0) -tuples_on u11)) . s1 by A36, Def5

.= o0 . sE by A40, FUNCT_1:47 ;

hence o1 . s in B by A10, A28, A35, A39, A37; :: thesis: verum

end;A37: P is_closed_on o0 by A6;

reconsider sE = s as Element of P * by A10, A28, FINSEQ_1:def 11;

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 A38, FINSEQ_2:def 4;

o1 . s = (o0 /. u11) . s1 by A29, A33, A34, Def6

.= (o0 | ((arity o0) -tuples_on u11)) . s1 by A36, Def5

.= o0 . sE by A40, FUNCT_1:47 ;

hence o1 . s in B by A10, A28, A35, A39, A37; :: thesis: verum

A42: dom the charact of U0 = dom (Opers (U0,P)) by Def6;

A43: P c= the carrier of U1 by A27, SETFAM_1:3;

now :: thesis: for n being Nat st n in dom the charact of U0 holds

the charact of E . n = (Opers (U1,B)) . n

hence
( the charact of E = Opers (U1,B) & B is opers_closed )
by A10, A29, A42, A30, A32, A41, FINSEQ_1:13; :: thesis: verumthe 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 A29, A30, A44, FUNCT_1:def 3;

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 A10, A42, A44, Def6

.= o0 | ((arity o0) -tuples_on P) by A46, Def5

.= o0 | (((arity o0) -tuples_on u11) /\ ((arity o0) -tuples_on P)) by A43, MARGREL1:21

.= (o0 | ((arity o0) -tuples_on u11)) | ((arity o0) -tuples_on P) by RELAT_1:71

.= (o0 /. u11) | ((arity o0) -tuples_on P) by A45, Def5

.= o1 | ((arity o0) -tuples_on P) by A29, A30, A44, Def6

.= o1 | ((arity o1) -tuples_on B) by A10, A28, A29, A30, A44, Th6

.= o1 /. B by A32, Def5

.= (Opers (U1,B)) . n by A29, A30, A41, A44, Def6 ; :: thesis: verum

end;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 A29, A30, A44, FUNCT_1:def 3;

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 A10, A42, A44, Def6

.= o0 | ((arity o0) -tuples_on P) by A46, Def5

.= o0 | (((arity o0) -tuples_on u11) /\ ((arity o0) -tuples_on P)) by A43, MARGREL1:21

.= (o0 | ((arity o0) -tuples_on u11)) | ((arity o0) -tuples_on P) by RELAT_1:71

.= (o0 /. u11) | ((arity o0) -tuples_on P) by A45, Def5

.= o1 | ((arity o0) -tuples_on P) by A29, A30, A44, Def6

.= o1 | ((arity o1) -tuples_on B) by A10, A28, A29, A30, A44, Th6

.= o1 /. B by A32, Def5

.= (Opers (U1,B)) . n by A29, A30, A41, A44, Def6 ; :: thesis: verum