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 Ideal of L1 holds
x is Ideal 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 Ideal of L1 holds
x is Ideal of L2
let x be set ; :: thesis: ( x is Ideal of L1 implies x is Ideal of L2 )
assume x is Ideal of L1 ; :: thesis: x is Ideal of L2
then reconsider F = x as Ideal 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 Lm1; :: thesis: verum

end;

hence x is Ideal of L2 by A1, Lm1; :: thesis: verum