:: UNIALG_2 semantic presentation

theorem Th1: :: UNIALG_2:1
for b1 being Nat
for b2 being non empty set
for b3 being non empty Subset of b2 holds (b1 -tuples_on b2) /\ (b1 -tuples_on b3) = b1 -tuples_on b3
proof end;

theorem Th2: :: UNIALG_2:2
for b1 being non empty set
for b2 being non empty homogeneous quasi_total PartFunc of b1 * ,b1 holds dom b2 = (arity b2) -tuples_on b1
proof end;

definition
let c1 be non empty set ;
mode PFuncsDomHQN of c1 -> non empty set means :Def1: :: UNIALG_2:def 1
for b1 being Element of a2 holds b1 is non empty homogeneous quasi_total PartFunc of a1 * ,a1;
existence
ex b1 being non empty set st
for b2 being Element of b1 holds b2 is non empty homogeneous quasi_total PartFunc of c1 * ,c1
proof end;
end;

:: deftheorem Def1 defines PFuncsDomHQN UNIALG_2:def 1 :
for b1, b2 being non empty set holds
( b2 is PFuncsDomHQN of b1 iff for b3 being Element of b2 holds b3 is non empty homogeneous quasi_total PartFunc of b1 * ,b1 );

definition
let c1 be non empty set ;
let c2 be PFuncsDomHQN of c1;
redefine mode Element as Element of c2 -> non empty homogeneous quasi_total PartFunc of a1 * ,a1;
coherence
for b1 being Element of c2 holds b1 is non empty homogeneous quasi_total PartFunc of c1 * ,c1
by Def1;
end;

definition
let c1 be Universal_Algebra;
mode PFuncsDomHQN of a1 is PFuncsDomHQN of the carrier of a1;
end;

definition
let c1 be UAStr ;
mode PartFunc of a1 is PartFunc of the carrier of a1 * ,the carrier of a1;
end;

definition
let c1, c2 be Universal_Algebra;
pred c1,c2 are_similar means :Def2: :: UNIALG_2:def 2
signature a1 = signature a2;
symmetry
for b1, b2 being Universal_Algebra st signature b1 = signature b2 holds
signature b2 = signature b1
;
reflexivity
for b1 being Universal_Algebra holds signature b1 = signature b1
;
end;

:: deftheorem Def2 defines are_similar UNIALG_2:def 2 :
for b1, b2 being Universal_Algebra holds
( b1,b2 are_similar iff signature b1 = signature b2 );

theorem Th3: :: UNIALG_2:3
for b1, b2 being Universal_Algebra st b1,b2 are_similar holds
len the charact of b1 = len the charact of b2
proof end;

theorem Th4: :: UNIALG_2:4
for b1, b2, b3 being Universal_Algebra st b1,b2 are_similar & b2,b3 are_similar holds
b1,b3 are_similar
proof end;

theorem Th5: :: UNIALG_2:5
for b1 being Universal_Algebra holds rng the charact of b1 is non empty Subset of (PFuncs (the carrier of b1 * ),the carrier of b1) by FINSEQ_1:27, FINSEQ_1:def 4;

definition
let c1 be Universal_Algebra;
func Operations c1 -> PFuncsDomHQN of a1 equals :: UNIALG_2:def 3
rng the charact of a1;
coherence
rng the charact of c1 is PFuncsDomHQN of c1
proof end;
end;

:: deftheorem Def3 defines Operations UNIALG_2:def 3 :
for b1 being Universal_Algebra holds Operations b1 = rng the charact of b1;

definition
let c1 be Universal_Algebra;
mode operation of a1 is Element of Operations a1;
end;

theorem Th6: :: UNIALG_2:6
for b1 being Universal_Algebra
for b2 being set st b2 in dom the charact of b1 holds
the charact of b1 . b2 is operation of b1 by FUNCT_1:def 5;

definition
let c1 be Universal_Algebra;
let c2 be Subset of c1;
let c3 be operation of c1;
pred c2 is_closed_on c3 means :Def4: :: UNIALG_2:def 4
for b1 being FinSequence of a2 st len b1 = arity a3 holds
a3 . b1 in a2;
end;

:: deftheorem Def4 defines is_closed_on UNIALG_2:def 4 :
for b1 being Universal_Algebra
for b2 being Subset of b1
for b3 being operation of b1 holds
( b2 is_closed_on b3 iff for b4 being FinSequence of b2 st len b4 = arity b3 holds
b3 . b4 in b2 );

definition
let c1 be Universal_Algebra;
let c2 be Subset of c1;
attr a2 is opers_closed means :Def5: :: UNIALG_2:def 5
for b1 being operation of a1 holds a2 is_closed_on b1;
end;

:: deftheorem Def5 defines opers_closed UNIALG_2:def 5 :
for b1 being Universal_Algebra
for b2 being Subset of b1 holds
( b2 is opers_closed iff for b3 being operation of b1 holds b2 is_closed_on b3 );

definition
let c1 be Universal_Algebra;
let c2 be non empty Subset of c1;
let c3 be operation of c1;
assume E8: c2 is_closed_on c3 ;
func c3 /. c2 -> non empty homogeneous quasi_total PartFunc of a2 * ,a2 equals :Def6: :: UNIALG_2:def 6
a3 | ((arity a3) -tuples_on a2);
coherence
c3 | ((arity c3) -tuples_on c2) is non empty homogeneous quasi_total PartFunc of c2 * ,c2
proof end;
end;

:: deftheorem Def6 defines /. UNIALG_2:def 6 :
for b1 being Universal_Algebra
for b2 being non empty Subset of b1
for b3 being operation of b1 st b2 is_closed_on b3 holds
b3 /. b2 = b3 | ((arity b3) -tuples_on b2);

definition
let c1 be Universal_Algebra;
let c2 be non empty Subset of c1;
func Opers c1,c2 -> PFuncFinSequence of a2 means :Def7: :: UNIALG_2:def 7
( dom a3 = dom the charact of a1 & ( for b1 being set
for b2 being operation of a1 st b1 in dom a3 & b2 = the charact of a1 . b1 holds
a3 . b1 = b2 /. a2 ) );
existence
ex b1 being PFuncFinSequence of c2 st
( dom b1 = dom the charact of c1 & ( for b2 being set
for b3 being operation of c1 st b2 in dom b1 & b3 = the charact of c1 . b2 holds
b1 . b2 = b3 /. c2 ) )
proof end;
uniqueness
for b1, b2 being PFuncFinSequence of c2 st dom b1 = dom the charact of c1 & ( for b3 being set
for b4 being operation of c1 st b3 in dom b1 & b4 = the charact of c1 . b3 holds
b1 . b3 = b4 /. c2 ) & dom b2 = dom the charact of c1 & ( for b3 being set
for b4 being operation of c1 st b3 in dom b2 & b4 = the charact of c1 . b3 holds
b2 . b3 = b4 /. c2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Opers UNIALG_2:def 7 :
for b1 being Universal_Algebra
for b2 being non empty Subset of b1
for b3 being PFuncFinSequence of b2 holds
( b3 = Opers b1,b2 iff ( dom b3 = dom the charact of b1 & ( for b4 being set
for b5 being operation of b1 st b4 in dom b3 & b5 = the charact of b1 . b4 holds
b3 . b4 = b5 /. b2 ) ) );

theorem Th7: :: UNIALG_2:7
for b1 being Universal_Algebra
for b2 being non empty Subset of b1 st b2 = the carrier of b1 holds
( b2 is opers_closed & ( for b3 being operation of b1 holds b3 /. b2 = b3 ) )
proof end;

theorem Th8: :: UNIALG_2:8
for b1 being Universal_Algebra
for b2 being non empty Subset of b1
for b3 being operation of b1 st b2 is_closed_on b3 holds
arity (b3 /. b2) = arity b3
proof end;

definition
let c1 be Universal_Algebra;
mode SubAlgebra of c1 -> Universal_Algebra means :Def8: :: UNIALG_2:def 8
( the carrier of a2 is Subset of a1 & ( for b1 being non empty Subset of a1 st b1 = the carrier of a2 holds
( the charact of a2 = Opers a1,b1 & b1 is opers_closed ) ) );
existence
ex b1 being Universal_Algebra st
( the carrier of b1 is Subset of c1 & ( for b2 being non empty Subset of c1 st b2 = the carrier of b1 holds
( the charact of b1 = Opers c1,b2 & b2 is opers_closed ) ) )
proof end;
end;

:: deftheorem Def8 defines SubAlgebra UNIALG_2:def 8 :
for b1, b2 being Universal_Algebra holds
( b2 is SubAlgebra of b1 iff ( the carrier of b2 is Subset of b1 & ( for b3 being non empty Subset of b1 st b3 = the carrier of b2 holds
( the charact of b2 = Opers b1,b3 & b3 is opers_closed ) ) ) );

registration
let c1 be Universal_Algebra;
cluster strict SubAlgebra of a1;
existence
ex b1 being SubAlgebra of c1 st b1 is strict
proof end;
end;

theorem Th9: :: UNIALG_2:9
for b1, b2 being Universal_Algebra
for b3 being operation of b1
for b4 being operation of b2
for b5 being Nat st b1 is SubAlgebra of b2 & b5 in dom the charact of b1 & b3 = the charact of b1 . b5 & b4 = the charact of b2 . b5 holds
arity b3 = arity b4
proof end;

theorem Th10: :: UNIALG_2:10
for b1, b2 being Universal_Algebra st b1 is SubAlgebra of b2 holds
dom the charact of b1 = dom the charact of b2
proof end;

theorem Th11: :: UNIALG_2:11
for b1 being Universal_Algebra holds b1 is SubAlgebra of b1
proof end;

theorem Th12: :: UNIALG_2:12
for b1, b2, b3 being Universal_Algebra st b1 is SubAlgebra of b2 & b2 is SubAlgebra of b3 holds
b1 is SubAlgebra of b3
proof end;

theorem Th13: :: UNIALG_2:13
for b1, b2 being Universal_Algebra st b1 is strict SubAlgebra of b2 & b2 is strict SubAlgebra of b1 holds
b1 = b2
proof end;

theorem Th14: :: UNIALG_2:14
for b1 being Universal_Algebra
for b2, b3 being SubAlgebra of b1 st the carrier of b2 c= the carrier of b3 holds
b2 is SubAlgebra of b3
proof end;

theorem Th15: :: UNIALG_2:15
for b1 being Universal_Algebra
for b2, b3 being strict SubAlgebra of b1 st the carrier of b2 = the carrier of b3 holds
b2 = b3
proof end;

theorem Th16: :: UNIALG_2:16
for b1, b2 being Universal_Algebra st b1 is SubAlgebra of b2 holds
b1,b2 are_similar
proof end;

theorem Th17: :: UNIALG_2:17
for b1 being Universal_Algebra
for b2 being non empty Subset of b1 holds UAStr(# b2,(Opers b1,b2) #) is strict Universal_Algebra
proof end;

definition
let c1 be Universal_Algebra;
let c2 be non empty Subset of c1;
assume E18: c2 is opers_closed ;
func UniAlgSetClosed c2 -> strict SubAlgebra of a1 equals :Def9: :: UNIALG_2:def 9
UAStr(# a2,(Opers a1,a2) #);
coherence
UAStr(# c2,(Opers c1,c2) #) is strict SubAlgebra of c1
proof end;
end;

:: deftheorem Def9 defines UniAlgSetClosed UNIALG_2:def 9 :
for b1 being Universal_Algebra
for b2 being non empty Subset of b1 st b2 is opers_closed holds
UniAlgSetClosed b2 = UAStr(# b2,(Opers b1,b2) #);

definition
let c1 be Universal_Algebra;
let c2, c3 be SubAlgebra of c1;
assume E19: the carrier of c2 meets the carrier of c3 ;
func c2 /\ c3 -> strict SubAlgebra of a1 means :Def10: :: UNIALG_2:def 10
( the carrier of a4 = the carrier of a2 /\ the carrier of a3 & ( for b1 being non empty Subset of a1 st b1 = the carrier of a4 holds
( the charact of a4 = Opers a1,b1 & b1 is opers_closed ) ) );
existence
ex b1 being strict SubAlgebra of c1 st
( the carrier of b1 = the carrier of c2 /\ the carrier of c3 & ( for b2 being non empty Subset of c1 st b2 = the carrier of b1 holds
( the charact of b1 = Opers c1,b2 & b2 is opers_closed ) ) )
proof end;
uniqueness
for b1, b2 being strict SubAlgebra of c1 st the carrier of b1 = the carrier of c2 /\ the carrier of c3 & ( for b3 being non empty Subset of c1 st b3 = the carrier of b1 holds
( the charact of b1 = Opers c1,b3 & b3 is opers_closed ) ) & the carrier of b2 = the carrier of c2 /\ the carrier of c3 & ( for b3 being non empty Subset of c1 st b3 = the carrier of b2 holds
( the charact of b2 = Opers c1,b3 & b3 is opers_closed ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines /\ UNIALG_2:def 10 :
for b1 being Universal_Algebra
for b2, b3 being SubAlgebra of b1 st the carrier of b2 meets the carrier of b3 holds
for b4 being strict SubAlgebra of b1 holds
( b4 = b2 /\ b3 iff ( the carrier of b4 = the carrier of b2 /\ the carrier of b3 & ( for b5 being non empty Subset of b1 st b5 = the carrier of b4 holds
( the charact of b4 = Opers b1,b5 & b5 is opers_closed ) ) ) );

definition
let c1 be Universal_Algebra;
func Constants c1 -> Subset of a1 equals :: UNIALG_2:def 11
{ b1 where B is Element of a1 : ex b1 being operation of a1 st
( arity b2 = 0 & b1 in rng b2 )
}
;
coherence
{ b1 where B is Element of c1 : ex b1 being operation of c1 st
( arity b2 = 0 & b1 in rng b2 )
}
is Subset of c1
proof end;
end;

:: deftheorem Def11 defines Constants UNIALG_2:def 11 :
for b1 being Universal_Algebra holds Constants b1 = { b2 where B is Element of b1 : ex b1 being operation of b1 st
( arity b3 = 0 & b2 in rng b3 )
}
;

definition
let c1 be Universal_Algebra;
attr a1 is with_const_op means :Def12: :: UNIALG_2:def 12
ex b1 being operation of a1 st arity b1 = 0;
end;

:: deftheorem Def12 defines with_const_op UNIALG_2:def 12 :
for b1 being Universal_Algebra holds
( b1 is with_const_op iff ex b2 being operation of b1 st arity b2 = 0 );

registration
cluster strict with_const_op UAStr ;
existence
ex b1 being Universal_Algebra st
( b1 is with_const_op & b1 is strict )
proof end;
end;

registration
let c1 be with_const_op Universal_Algebra;
cluster Constants a1 -> non empty ;
coherence
not Constants c1 is empty
proof end;
end;

theorem Th18: :: UNIALG_2:18
for b1 being Universal_Algebra
for b2 being SubAlgebra of b1 holds Constants b1 is Subset of b2
proof end;

theorem Th19: :: UNIALG_2:19
for b1 being with_const_op Universal_Algebra
for b2 being SubAlgebra of b1 holds Constants b1 is non empty Subset of b2 by Th18;

theorem Th20: :: UNIALG_2:20
for b1 being with_const_op Universal_Algebra
for b2, b3 being SubAlgebra of b1 holds the carrier of b2 meets the carrier of b3
proof end;

definition
let c1 be Universal_Algebra;
let c2 be Subset of c1;
assume E23: ( Constants c1 <> {} or c2 <> {} ) ;
func GenUnivAlg c2 -> strict SubAlgebra of a1 means :Def13: :: UNIALG_2:def 13
( a2 c= the carrier of a3 & ( for b1 being SubAlgebra of a1 st a2 c= the carrier of b1 holds
a3 is SubAlgebra of b1 ) );
existence
ex b1 being strict SubAlgebra of c1 st
( c2 c= the carrier of b1 & ( for b2 being SubAlgebra of c1 st c2 c= the carrier of b2 holds
b1 is SubAlgebra of b2 ) )
proof end;
uniqueness
for b1, b2 being strict SubAlgebra of c1 st c2 c= the carrier of b1 & ( for b3 being SubAlgebra of c1 st c2 c= the carrier of b3 holds
b1 is SubAlgebra of b3 ) & c2 c= the carrier of b2 & ( for b3 being SubAlgebra of c1 st c2 c= the carrier of b3 holds
b2 is SubAlgebra of b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines GenUnivAlg UNIALG_2:def 13 :
for b1 being Universal_Algebra
for b2 being Subset of b1 st ( Constants b1 <> {} or b2 <> {} ) holds
for b3 being strict SubAlgebra of b1 holds
( b3 = GenUnivAlg b2 iff ( b2 c= the carrier of b3 & ( for b4 being SubAlgebra of b1 st b2 c= the carrier of b4 holds
b3 is SubAlgebra of b4 ) ) );

theorem Th21: :: UNIALG_2:21
for b1 being strict Universal_Algebra holds GenUnivAlg ([#] the carrier of b1) = b1
proof end;

theorem Th22: :: UNIALG_2:22
for b1 being Universal_Algebra
for b2 being strict SubAlgebra of b1
for b3 being non empty Subset of b1 st b3 = the carrier of b2 holds
GenUnivAlg b3 = b2
proof end;

definition
let c1 be Universal_Algebra;
let c2, c3 be SubAlgebra of c1;
func c2 "\/" c3 -> strict SubAlgebra of a1 means :Def14: :: UNIALG_2:def 14
for b1 being non empty Subset of a1 st b1 = the carrier of a2 \/ the carrier of a3 holds
a4 = GenUnivAlg b1;
existence
ex b1 being strict SubAlgebra of c1 st
for b2 being non empty Subset of c1 st b2 = the carrier of c2 \/ the carrier of c3 holds
b1 = GenUnivAlg b2
proof end;
uniqueness
for b1, b2 being strict SubAlgebra of c1 st ( for b3 being non empty Subset of c1 st b3 = the carrier of c2 \/ the carrier of c3 holds
b1 = GenUnivAlg b3 ) & ( for b3 being non empty Subset of c1 st b3 = the carrier of c2 \/ the carrier of c3 holds
b2 = GenUnivAlg b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines "\/" UNIALG_2:def 14 :
for b1 being Universal_Algebra
for b2, b3 being SubAlgebra of b1
for b4 being strict SubAlgebra of b1 holds
( b4 = b2 "\/" b3 iff for b5 being non empty Subset of b1 st b5 = the carrier of b2 \/ the carrier of b3 holds
b4 = GenUnivAlg b5 );

theorem Th23: :: UNIALG_2:23
for b1 being Universal_Algebra
for b2 being SubAlgebra of b1
for b3, b4 being Subset of b1 st ( b3 <> {} or Constants b1 <> {} ) & b4 = b3 \/ the carrier of b2 holds
(GenUnivAlg b3) "\/" b2 = GenUnivAlg b4
proof end;

theorem Th24: :: UNIALG_2:24
for b1 being Universal_Algebra
for b2, b3 being SubAlgebra of b1 holds b2 "\/" b3 = b3 "\/" b2
proof end;

theorem Th25: :: UNIALG_2:25
for b1 being with_const_op Universal_Algebra
for b2, b3 being strict SubAlgebra of b1 holds b2 /\ (b2 "\/" b3) = b2
proof end;

theorem Th26: :: UNIALG_2:26
for b1 being with_const_op Universal_Algebra
for b2, b3 being strict SubAlgebra of b1 holds (b2 /\ b3) "\/" b3 = b3
proof end;

definition
let c1 be Universal_Algebra;
func Sub c1 -> set means :Def15: :: UNIALG_2:def 15
for b1 being set holds
( b1 in a2 iff b1 is strict SubAlgebra of a1 );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff b2 is strict SubAlgebra of c1 )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff b3 is strict SubAlgebra of c1 ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is strict SubAlgebra of c1 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines Sub UNIALG_2:def 15 :
for b1 being Universal_Algebra
for b2 being set holds
( b2 = Sub b1 iff for b3 being set holds
( b3 in b2 iff b3 is strict SubAlgebra of b1 ) );

registration
let c1 be Universal_Algebra;
cluster Sub a1 -> non empty ;
coherence
not Sub c1 is empty
proof end;
end;

definition
let c1 be Universal_Algebra;
func UniAlg_join c1 -> BinOp of Sub a1 means :Def16: :: UNIALG_2:def 16
for b1, b2 being Element of Sub a1
for b3, b4 being strict SubAlgebra of a1 st b1 = b3 & b2 = b4 holds
a2 . b1,b2 = b3 "\/" b4;
existence
ex b1 being BinOp of Sub c1 st
for b2, b3 being Element of Sub c1
for b4, b5 being strict SubAlgebra of c1 st b2 = b4 & b3 = b5 holds
b1 . b2,b3 = b4 "\/" b5
proof end;
uniqueness
for b1, b2 being BinOp of Sub c1 st ( for b3, b4 being Element of Sub c1
for b5, b6 being strict SubAlgebra of c1 st b3 = b5 & b4 = b6 holds
b1 . b3,b4 = b5 "\/" b6 ) & ( for b3, b4 being Element of Sub c1
for b5, b6 being strict SubAlgebra of c1 st b3 = b5 & b4 = b6 holds
b2 . b3,b4 = b5 "\/" b6 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines UniAlg_join UNIALG_2:def 16 :
for b1 being Universal_Algebra
for b2 being BinOp of Sub b1 holds
( b2 = UniAlg_join b1 iff for b3, b4 being Element of Sub b1
for b5, b6 being strict SubAlgebra of b1 st b3 = b5 & b4 = b6 holds
b2 . b3,b4 = b5 "\/" b6 );

definition
let c1 be Universal_Algebra;
func UniAlg_meet c1 -> BinOp of Sub a1 means :Def17: :: UNIALG_2:def 17
for b1, b2 being Element of Sub a1
for b3, b4 being strict SubAlgebra of a1 st b1 = b3 & b2 = b4 holds
a2 . b1,b2 = b3 /\ b4;
existence
ex b1 being BinOp of Sub c1 st
for b2, b3 being Element of Sub c1
for b4, b5 being strict SubAlgebra of c1 st b2 = b4 & b3 = b5 holds
b1 . b2,b3 = b4 /\ b5
proof end;
uniqueness
for b1, b2 being BinOp of Sub c1 st ( for b3, b4 being Element of Sub c1
for b5, b6 being strict SubAlgebra of c1 st b3 = b5 & b4 = b6 holds
b1 . b3,b4 = b5 /\ b6 ) & ( for b3, b4 being Element of Sub c1
for b5, b6 being strict SubAlgebra of c1 st b3 = b5 & b4 = b6 holds
b2 . b3,b4 = b5 /\ b6 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines UniAlg_meet UNIALG_2:def 17 :
for b1 being Universal_Algebra
for b2 being BinOp of Sub b1 holds
( b2 = UniAlg_meet b1 iff for b3, b4 being Element of Sub b1
for b5, b6 being strict SubAlgebra of b1 st b3 = b5 & b4 = b6 holds
b2 . b3,b4 = b5 /\ b6 );

theorem Th27: :: UNIALG_2:27
for b1 being Universal_Algebra holds UniAlg_join b1 is commutative
proof end;

theorem Th28: :: UNIALG_2:28
for b1 being Universal_Algebra holds UniAlg_join b1 is associative
proof end;

theorem Th29: :: UNIALG_2:29
for b1 being with_const_op Universal_Algebra holds UniAlg_meet b1 is commutative
proof end;

theorem Th30: :: UNIALG_2:30
for b1 being with_const_op Universal_Algebra holds UniAlg_meet b1 is associative
proof end;

definition
let c1 be with_const_op Universal_Algebra;
func UnSubAlLattice c1 -> strict Lattice equals :: UNIALG_2:def 18
LattStr(# (Sub a1),(UniAlg_join a1),(UniAlg_meet a1) #);
coherence
LattStr(# (Sub c1),(UniAlg_join c1),(UniAlg_meet c1) #) is strict Lattice
proof end;
end;

:: deftheorem Def18 defines UnSubAlLattice UNIALG_2:def 18 :
for b1 being with_const_op Universal_Algebra holds UnSubAlLattice b1 = LattStr(# (Sub b1),(UniAlg_join b1),(UniAlg_meet b1) #);