begin
definition
let L be
Lattice;
let F be
Filter of
L;
uniqueness
for b1, b2 being Lattice st ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & b1 = LattStr(# F,o1,o2 #) ) & ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & b2 = LattStr(# F,o1,o2 #) ) holds
b1 = b2
;
existence
ex b1 being Lattice ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & b1 = LattStr(# F,o1,o2 #) )
end;
theorem
for
B being
B_Lattice for
FB being
Filter of
B for
I being
I_Lattice for
i,
j,
k being
Element of
I for
FI being
Filter of
I for
a,
b,
c being
Element of
B holds
( (
i,
j are_equivalence_wrt FI &
j,
k are_equivalence_wrt FI implies
i,
k are_equivalence_wrt FI ) & (
a,
b are_equivalence_wrt FB &
b,
c are_equivalence_wrt FB implies
a,
c are_equivalence_wrt FB ) )
begin