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

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

end;

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