let L1, L2 be Lattice; ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for x being set st x is Filter of L1 holds
x is Filter of L2 )
assume A1:
LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #)
; for x being set st x is Filter of L1 holds
x is Filter of L2
let x be set ; ( x is Filter of L1 implies x is Filter of L2 )
assume
x is Filter of L1
; x is Filter of L2
then reconsider F = x as Filter of L1 ;
hence
x is Filter of L2
by A1, FILTER_0:8; verum