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 Def16;
hence latt F = latt L,F by FILTER_0:def 10; :: thesis: verum