let L be Lattice; for p, q being Element of L
for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let p, q be Element of L; for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let F be Filter of L; for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let p9, q9 be Element of (latt F); ( p = p9 & q = q9 implies ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) )
assume A1:
( p = p9 & q = q9 )
; ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
consider o1, o2 being BinOp of F such that
A2:
o1 = the L_join of L || F
and
A3:
o2 = the L_meet of L || F
and
A4:
latt F = LattStr(# F,o1,o2 #)
by Def9;
dom o1 = [:F,F:]
by FUNCT_2:def 1;
then
[p,q] in dom o1
by A1, A4, ZFMISC_1:87;
hence
p "\/" q = p9 "\/" q9
by A1, A2, A4, FUNCT_1:47; p "/\" q = p9 "/\" q9
dom o2 = [:F,F:]
by FUNCT_2:def 1;
then
[p,q] in dom o2
by A1, A4, ZFMISC_1:87;
hence
p "/\" q = p9 "/\" q9
by A1, A3, A4, FUNCT_1:47; verum