let L be Lattice; :: thesis: for F being Filter of L holds latt F = latt (L,F)
let F be Filter of L; :: thesis: latt F = latt (L,F)
ex o1, o2 being BinOp of F st
( o1 = H₂(L) || F & o2 = H₃(L) || F & latt (L,F) = LattStr(# F,o1,o2 #) ) by Def14;
hence latt F = latt (L,F) by FILTER_0:def 9; :: thesis: verum