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