let L1, L2 be Lattice; :: thesis: ( 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 #) ; :: thesis: for x being set st x is Filter of L1 holds
x is Filter of L2
let x be set ; :: thesis: ( x is Filter of L1 implies x is Filter of L2 )
assume x is Filter of L1 ; :: thesis: x is Filter of L2
then reconsider F = x as Filter of L1 ;

now :: thesis: for a, b being Element of L2 holds
( ( a in F & b in F ) iff a "/\" b in F )

let a, b be Element of L2; :: thesis: ( ( a in F & b in F ) iff a "/\" b in F )
reconsider a9 = a, b9 = b as Element of L1 by A1;
a "/\" b = a9 "/\" b9 by A1;
hence ( ( a in F & b in F ) iff a "/\" b in F ) by FILTER_0:8; :: thesis: verum

end;

hence x is Filter of L2 by A1, FILTER_0:8; :: thesis: verum