:: by Ewa Burakowska

::

:: Received July 8, 1993

:: Copyright (c) 1993-2012 Association of Mizar Users

begin

definition
end;

definition
end;

definition

let U1, U2 be Universal_Algebra;

symmetry

for U1, U2 being Universal_Algebra st signature U1 = signature U2 holds

signature U2 = signature U1 ;

reflexivity

for U1 being Universal_Algebra holds signature U1 = signature U1 ;

end;
symmetry

for U1, U2 being Universal_Algebra st signature U1 = signature U2 holds

signature U2 = signature U1 ;

reflexivity

for U1 being Universal_Algebra holds signature U1 = signature U1 ;

:: deftheorem Def1 defines are_similar UNIALG_2:def 1 :

for U1, U2 being Universal_Algebra holds

( U1,U2 are_similar iff signature U1 = signature U2 );

for U1, U2 being Universal_Algebra holds

( U1,U2 are_similar iff signature U1 = signature U2 );

theorem :: UNIALG_2:1

for U1, U2 being Universal_Algebra st U1,U2 are_similar holds

len the charact of U1 = len the charact of U2

len the charact of U1 = len the charact of U2

proof end;

theorem :: UNIALG_2:2

for U1, U2, U3 being Universal_Algebra st U1,U2 are_similar & U2,U3 are_similar holds

U1,U3 are_similar

U1,U3 are_similar

proof end;

theorem :: UNIALG_2:3

for U0 being Universal_Algebra holds rng the charact of U0 is non empty Subset of (PFuncs (( the carrier of U0 *), the carrier of U0)) by FINSEQ_1:def 4, RELAT_1:41;

definition
end;

:: deftheorem defines Operations UNIALG_2:def 2 :

for U0 being Universal_Algebra holds Operations U0 = rng the charact of U0;

for U0 being Universal_Algebra holds Operations U0 = rng the charact of U0;

definition

let U0 be Universal_Algebra;

let A be Subset of U0;

let o be operation of U0;

end;
let A be Subset of U0;

let o be operation of U0;

pred A is_closed_on o means :Def3: :: UNIALG_2:def 3

for s being FinSequence of A st len s = arity o holds

o . s in A;

for s being FinSequence of A st len s = arity o holds

o . s in A;

:: deftheorem Def3 defines is_closed_on UNIALG_2:def 3 :

for U0 being Universal_Algebra

for A being Subset of U0

for o being operation of U0 holds

( A is_closed_on o iff for s being FinSequence of A st len s = arity o holds

o . s in A );

for U0 being Universal_Algebra

for A being Subset of U0

for o being operation of U0 holds

( A is_closed_on o iff for s being FinSequence of A st len s = arity o holds

o . s in A );

definition

let U0 be Universal_Algebra;

let A be Subset of U0;

end;
let A be Subset of U0;

attr A is opers_closed means :Def4: :: UNIALG_2:def 4

for o being operation of U0 holds A is_closed_on o;

for o being operation of U0 holds A is_closed_on o;

:: deftheorem Def4 defines opers_closed UNIALG_2:def 4 :

for U0 being Universal_Algebra

for A being Subset of U0 holds

( A is opers_closed iff for o being operation of U0 holds A is_closed_on o );

for U0 being Universal_Algebra

for A being Subset of U0 holds

( A is opers_closed iff for o being operation of U0 holds A is_closed_on o );

definition

let U0 be Universal_Algebra;

let A be non empty Subset of U0;

let o be operation of U0;

assume A1: A is_closed_on o ;

o | ((arity o) -tuples_on A) is non empty homogeneous quasi_total PartFunc of (A *),A

end;
let A be non empty Subset of U0;

let o be operation of U0;

assume A1: A is_closed_on o ;

func o /. A -> non empty homogeneous quasi_total PartFunc of (A *),A equals :Def5: :: UNIALG_2:def 5

o | ((arity o) -tuples_on A);

coherence o | ((arity o) -tuples_on A);

o | ((arity o) -tuples_on A) is non empty homogeneous quasi_total PartFunc of (A *),A

proof end;

:: deftheorem Def5 defines /. UNIALG_2:def 5 :

for U0 being Universal_Algebra

for A being non empty Subset of U0

for o being operation of U0 st A is_closed_on o holds

o /. A = o | ((arity o) -tuples_on A);

for U0 being Universal_Algebra

for A being non empty Subset of U0

for o being operation of U0 st A is_closed_on o holds

o /. A = o | ((arity o) -tuples_on A);

definition

let U0 be Universal_Algebra;

let A be non empty Subset of U0;

ex b_{1} being PFuncFinSequence of A st

( dom b_{1} = dom the charact of U0 & ( for n being set

for o being operation of U0 st n in dom b_{1} & o = the charact of U0 . n holds

b_{1} . n = o /. A ) )

for b_{1}, b_{2} being PFuncFinSequence of A st dom b_{1} = dom the charact of U0 & ( for n being set

for o being operation of U0 st n in dom b_{1} & o = the charact of U0 . n holds

b_{1} . n = o /. A ) & dom b_{2} = dom the charact of U0 & ( for n being set

for o being operation of U0 st n in dom b_{2} & o = the charact of U0 . n holds

b_{2} . n = o /. A ) holds

b_{1} = b_{2}

end;
let A be non empty Subset of U0;

func Opers (U0,A) -> PFuncFinSequence of A means :Def6: :: UNIALG_2:def 6

( dom it = dom the charact of U0 & ( for n being set

for o being operation of U0 st n in dom it & o = the charact of U0 . n holds

it . n = o /. A ) );

existence ( dom it = dom the charact of U0 & ( for n being set

for o being operation of U0 st n in dom it & o = the charact of U0 . n holds

it . n = o /. A ) );

ex b

( dom b

for o being operation of U0 st n in dom b

b

proof end;

uniqueness for b

for o being operation of U0 st n in dom b

b

for o being operation of U0 st n in dom b

b

b

proof end;

:: deftheorem Def6 defines Opers UNIALG_2:def 6 :

for U0 being Universal_Algebra

for A being non empty Subset of U0

for b_{3} being PFuncFinSequence of A holds

( b_{3} = Opers (U0,A) iff ( dom b_{3} = dom the charact of U0 & ( for n being set

for o being operation of U0 st n in dom b_{3} & o = the charact of U0 . n holds

b_{3} . n = o /. A ) ) );

for U0 being Universal_Algebra

for A being non empty Subset of U0

for b

( b

for o being operation of U0 st n in dom b

b

theorem Th4: :: UNIALG_2:4

for U0 being Universal_Algebra

for B being non empty Subset of U0 st B = the carrier of U0 holds

( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) )

for B being non empty Subset of U0 st B = the carrier of U0 holds

( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) )

proof end;

theorem :: UNIALG_2:5

for U1 being Universal_Algebra

for A being non empty Subset of U1

for o being operation of U1 st A is_closed_on o holds

arity (o /. A) = arity o

for A being non empty Subset of U1

for o being operation of U1 st A is_closed_on o holds

arity (o /. A) = arity o

proof end;

definition

let U0 be Universal_Algebra;

ex b_{1} being Universal_Algebra st

( the carrier of b_{1} is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of b_{1} holds

( the charact of b_{1} = Opers (U0,B) & B is opers_closed ) ) )

end;
mode SubAlgebra of U0 -> Universal_Algebra means :Def7: :: UNIALG_2:def 7

( the carrier of it is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of it holds

( the charact of it = Opers (U0,B) & B is opers_closed ) ) );

existence ( the carrier of it is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of it holds

( the charact of it = Opers (U0,B) & B is opers_closed ) ) );

ex b

( the carrier of b

( the charact of b

proof end;

:: deftheorem Def7 defines SubAlgebra UNIALG_2:def 7 :

for U0, b_{2} being Universal_Algebra holds

( b_{2} is SubAlgebra of U0 iff ( the carrier of b_{2} is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of b_{2} holds

( the charact of b_{2} = Opers (U0,B) & B is opers_closed ) ) ) );

for U0, b

( b

( the charact of b

registration

let U0 be Universal_Algebra;

existence

ex b_{1} being SubAlgebra of U0 st b_{1} is strict

end;
existence

ex b

proof end;

theorem Th6: :: UNIALG_2:6

for U0, U1 being Universal_Algebra

for o0 being operation of U0

for o1 being operation of U1

for n being Nat st U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n holds

arity o0 = arity o1

for o0 being operation of U0

for o1 being operation of U1

for n being Nat st U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n holds

arity o0 = arity o1

proof end;

theorem Th7: :: UNIALG_2:7

for U0, U1 being Universal_Algebra st U0 is SubAlgebra of U1 holds

dom the charact of U0 = dom the charact of U1

dom the charact of U0 = dom the charact of U1

proof end;

theorem :: UNIALG_2:9

for U0, U1, U2 being Universal_Algebra st U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 holds

U0 is SubAlgebra of U2

U0 is SubAlgebra of U2

proof end;

theorem Th10: :: UNIALG_2:10

for U1, U2 being Universal_Algebra st U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 holds

U1 = U2

U1 = U2

proof end;

theorem Th11: :: UNIALG_2:11

for U0 being Universal_Algebra

for U1, U2 being SubAlgebra of U0 st the carrier of U1 c= the carrier of U2 holds

U1 is SubAlgebra of U2

for U1, U2 being SubAlgebra of U0 st the carrier of U1 c= the carrier of U2 holds

U1 is SubAlgebra of U2

proof end;

theorem Th12: :: UNIALG_2:12

for U0 being Universal_Algebra

for U1, U2 being strict SubAlgebra of U0 st the carrier of U1 = the carrier of U2 holds

U1 = U2

for U1, U2 being strict SubAlgebra of U0 st the carrier of U1 = the carrier of U2 holds

U1 = U2

proof end;

theorem Th14: :: UNIALG_2:14

for U0 being Universal_Algebra

for A being non empty Subset of U0 holds UAStr(# A,(Opers (U0,A)) #) is strict Universal_Algebra

for A being non empty Subset of U0 holds UAStr(# A,(Opers (U0,A)) #) is strict Universal_Algebra

proof end;

definition

let U0 be Universal_Algebra;

let A be non empty Subset of U0;

assume A1: A is opers_closed ;

UAStr(# A,(Opers (U0,A)) #) is strict SubAlgebra of U0

end;
let A be non empty Subset of U0;

assume A1: A is opers_closed ;

func UniAlgSetClosed A -> strict SubAlgebra of U0 equals :Def8: :: UNIALG_2:def 8

UAStr(# A,(Opers (U0,A)) #);

coherence UAStr(# A,(Opers (U0,A)) #);

UAStr(# A,(Opers (U0,A)) #) is strict SubAlgebra of U0

proof end;

:: deftheorem Def8 defines UniAlgSetClosed UNIALG_2:def 8 :

for U0 being Universal_Algebra

for A being non empty Subset of U0 st A is opers_closed holds

UniAlgSetClosed A = UAStr(# A,(Opers (U0,A)) #);

for U0 being Universal_Algebra

for A being non empty Subset of U0 st A is opers_closed holds

UniAlgSetClosed A = UAStr(# A,(Opers (U0,A)) #);

definition

let U0 be Universal_Algebra;

let U1, U2 be SubAlgebra of U0;

assume A1: the carrier of U1 meets the carrier of U2 ;

ex b_{1} being strict SubAlgebra of U0 st

( the carrier of b_{1} = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b_{1} holds

( the charact of b_{1} = Opers (U0,B) & B is opers_closed ) ) )

for b_{1}, b_{2} being strict SubAlgebra of U0 st the carrier of b_{1} = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b_{1} holds

( the charact of b_{1} = Opers (U0,B) & B is opers_closed ) ) & the carrier of b_{2} = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b_{2} holds

( the charact of b_{2} = Opers (U0,B) & B is opers_closed ) ) holds

b_{1} = b_{2}

end;
let U1, U2 be SubAlgebra of U0;

assume A1: the carrier of U1 meets the carrier of U2 ;

func U1 /\ U2 -> strict SubAlgebra of U0 means :Def9: :: UNIALG_2:def 9

( the carrier of it = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of it holds

( the charact of it = Opers (U0,B) & B is opers_closed ) ) );

existence ( the carrier of it = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of it holds

( the charact of it = Opers (U0,B) & B is opers_closed ) ) );

ex b

( the carrier of b

( the charact of b

proof end;

uniqueness for b

( the charact of b

( the charact of b

b

proof end;

:: deftheorem Def9 defines /\ UNIALG_2:def 9 :

for U0 being Universal_Algebra

for U1, U2 being SubAlgebra of U0 st the carrier of U1 meets the carrier of U2 holds

for b_{4} being strict SubAlgebra of U0 holds

( b_{4} = U1 /\ U2 iff ( the carrier of b_{4} = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b_{4} holds

( the charact of b_{4} = Opers (U0,B) & B is opers_closed ) ) ) );

for U0 being Universal_Algebra

for U1, U2 being SubAlgebra of U0 st the carrier of U1 meets the carrier of U2 holds

for b

( b

( the charact of b

definition

let U0 be Universal_Algebra;

{ a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } is Subset of U0

end;
func Constants U0 -> Subset of U0 equals :: UNIALG_2:def 10

{ a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } ;

coherence { a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } ;

{ a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } is Subset of U0

proof end;

:: deftheorem defines Constants UNIALG_2:def 10 :

for U0 being Universal_Algebra holds Constants U0 = { a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } ;

for U0 being Universal_Algebra holds Constants U0 = { a where a is Element of U0 : ex o being operation of U0 st

( arity o = 0 & a in rng o ) } ;

definition

let IT be Universal_Algebra;

end;
attr IT is with_const_op means :Def11: :: UNIALG_2:def 11

ex o being operation of IT st arity o = 0 ;

ex o being operation of IT st arity o = 0 ;

:: deftheorem Def11 defines with_const_op UNIALG_2:def 11 :

for IT being Universal_Algebra holds

( IT is with_const_op iff ex o being operation of IT st arity o = 0 );

for IT being Universal_Algebra holds

( IT is with_const_op iff ex o being operation of IT st arity o = 0 );

registration

existence

ex b_{1} being Universal_Algebra st

( b_{1} is with_const_op & b_{1} is strict )

end;
ex b

( b

proof end;

registration
end;

theorem :: UNIALG_2:16

for U0 being with_const_op Universal_Algebra

for U1 being SubAlgebra of U0 holds Constants U0 is non empty Subset of U1 by Th15;

for U1 being SubAlgebra of U0 holds Constants U0 is non empty Subset of U1 by Th15;

theorem Th17: :: UNIALG_2:17

for U0 being with_const_op Universal_Algebra

for U1, U2 being SubAlgebra of U0 holds the carrier of U1 meets the carrier of U2

for U1, U2 being SubAlgebra of U0 holds the carrier of U1 meets the carrier of U2

proof end;

definition

let U0 be Universal_Algebra;

let A be Subset of U0;

assume A1: ( Constants U0 <> {} or A <> {} ) ;

ex b_{1} being strict SubAlgebra of U0 st

( A c= the carrier of b_{1} & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds

b_{1} is SubAlgebra of U1 ) )

for b_{1}, b_{2} being strict SubAlgebra of U0 st A c= the carrier of b_{1} & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds

b_{1} is SubAlgebra of U1 ) & A c= the carrier of b_{2} & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds

b_{2} is SubAlgebra of U1 ) holds

b_{1} = b_{2}

end;
let A be Subset of U0;

assume A1: ( Constants U0 <> {} or A <> {} ) ;

func GenUnivAlg A -> strict SubAlgebra of U0 means :Def12: :: UNIALG_2:def 12

( A c= the carrier of it & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds

it is SubAlgebra of U1 ) );

existence ( A c= the carrier of it & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds

it is SubAlgebra of U1 ) );

ex b

( A c= the carrier of b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def12 defines GenUnivAlg UNIALG_2:def 12 :

for U0 being Universal_Algebra

for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds

for b_{3} being strict SubAlgebra of U0 holds

( b_{3} = GenUnivAlg A iff ( A c= the carrier of b_{3} & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds

b_{3} is SubAlgebra of U1 ) ) );

for U0 being Universal_Algebra

for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds

for b

( b

b

theorem Th19: :: UNIALG_2:19

for U0 being Universal_Algebra

for U1 being strict SubAlgebra of U0

for B being non empty Subset of U0 st B = the carrier of U1 holds

GenUnivAlg B = U1

for U1 being strict SubAlgebra of U0

for B being non empty Subset of U0 st B = the carrier of U1 holds

GenUnivAlg B = U1

proof end;

definition

let U0 be Universal_Algebra;

let U1, U2 be SubAlgebra of U0;

ex b_{1} being strict SubAlgebra of U0 st

for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

b_{1} = GenUnivAlg A

for b_{1}, b_{2} being strict SubAlgebra of U0 st ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

b_{1} = GenUnivAlg A ) & ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

b_{2} = GenUnivAlg A ) holds

b_{1} = b_{2}

end;
let U1, U2 be SubAlgebra of U0;

func U1 "\/" U2 -> strict SubAlgebra of U0 means :Def13: :: UNIALG_2:def 13

for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

it = GenUnivAlg A;

existence for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

it = GenUnivAlg A;

ex b

for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def13 defines "\/" UNIALG_2:def 13 :

for U0 being Universal_Algebra

for U1, U2 being SubAlgebra of U0

for b_{4} being strict SubAlgebra of U0 holds

( b_{4} = U1 "\/" U2 iff for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

b_{4} = GenUnivAlg A );

for U0 being Universal_Algebra

for U1, U2 being SubAlgebra of U0

for b

( b

b

theorem Th20: :: UNIALG_2:20

for U0 being Universal_Algebra

for U1 being SubAlgebra of U0

for A, B being Subset of U0 st ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 holds

(GenUnivAlg A) "\/" U1 = GenUnivAlg B

for U1 being SubAlgebra of U0

for A, B being Subset of U0 st ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 holds

(GenUnivAlg A) "\/" U1 = GenUnivAlg B

proof end;

theorem Th22: :: UNIALG_2:22

for U0 being with_const_op Universal_Algebra

for U1, U2 being strict SubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = U1

for U1, U2 being strict SubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = U1

proof end;

theorem Th23: :: UNIALG_2:23

for U0 being with_const_op Universal_Algebra

for U1, U2 being strict SubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = U2

for U1, U2 being strict SubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = U2

proof end;

definition

let U0 be Universal_Algebra;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is strict SubAlgebra of U0 )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is strict SubAlgebra of U0 ) ) & ( for x being set holds

( x in b_{2} iff x is strict SubAlgebra of U0 ) ) holds

b_{1} = b_{2}

end;
func Sub U0 -> set means :Def14: :: UNIALG_2:def 14

for x being set holds

( x in it iff x is strict SubAlgebra of U0 );

existence for x being set holds

( x in it iff x is strict SubAlgebra of U0 );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def14 defines Sub UNIALG_2:def 14 :

for U0 being Universal_Algebra

for b_{2} being set holds

( b_{2} = Sub U0 iff for x being set holds

( x in b_{2} iff x is strict SubAlgebra of U0 ) );

for U0 being Universal_Algebra

for b

( b

( x in b

registration
end;

definition

let U0 be Universal_Algebra;

ex b_{1} being BinOp of (Sub U0) st

for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b_{1} . (x,y) = U1 "\/" U2

for b_{1}, b_{2} being BinOp of (Sub U0) st ( for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b_{1} . (x,y) = U1 "\/" U2 ) & ( for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b_{2} . (x,y) = U1 "\/" U2 ) holds

b_{1} = b_{2}

end;
func UniAlg_join U0 -> BinOp of (Sub U0) means :Def15: :: UNIALG_2:def 15

for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

it . (x,y) = U1 "\/" U2;

existence for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

it . (x,y) = U1 "\/" U2;

ex b

for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b

proof end;

uniqueness for b

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b

b

proof end;

:: deftheorem Def15 defines UniAlg_join UNIALG_2:def 15 :

for U0 being Universal_Algebra

for b_{2} being BinOp of (Sub U0) holds

( b_{2} = UniAlg_join U0 iff for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b_{2} . (x,y) = U1 "\/" U2 );

for U0 being Universal_Algebra

for b

( b

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b

definition

let U0 be Universal_Algebra;

ex b_{1} being BinOp of (Sub U0) st

for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b_{1} . (x,y) = U1 /\ U2

for b_{1}, b_{2} being BinOp of (Sub U0) st ( for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b_{1} . (x,y) = U1 /\ U2 ) & ( for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b_{2} . (x,y) = U1 /\ U2 ) holds

b_{1} = b_{2}

end;
func UniAlg_meet U0 -> BinOp of (Sub U0) means :Def16: :: UNIALG_2:def 16

for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

it . (x,y) = U1 /\ U2;

existence for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

it . (x,y) = U1 /\ U2;

ex b

for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b

proof end;

uniqueness for b

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b

b

proof end;

:: deftheorem Def16 defines UniAlg_meet UNIALG_2:def 16 :

for U0 being Universal_Algebra

for b_{2} being BinOp of (Sub U0) holds

( b_{2} = UniAlg_meet U0 iff for x, y being Element of Sub U0

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b_{2} . (x,y) = U1 /\ U2 );

for U0 being Universal_Algebra

for b

( b

for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds

b

definition

let U0 be with_const_op Universal_Algebra;

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is strict Lattice

end;
func UnSubAlLattice U0 -> strict Lattice equals :: UNIALG_2:def 17

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #);

coherence LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #);

LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is strict Lattice

proof end;

:: deftheorem defines UnSubAlLattice UNIALG_2:def 17 :

for U0 being with_const_op Universal_Algebra holds UnSubAlLattice U0 = LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #);

for U0 being with_const_op Universal_Algebra holds UnSubAlLattice U0 = LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #);