let L1, L2 be LATTICE; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for x being set st x is prime Ideal of L1 holds

x is prime Ideal of L2 )

assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: for x being set st x is prime Ideal of L1 holds

x is prime Ideal of L2

let x be set ; :: thesis: ( x is prime Ideal of L1 implies x is prime Ideal of L2 )

assume x is prime Ideal of L1 ; :: thesis: x is prime Ideal of L2

then reconsider I = x as prime Ideal of L1 ;

reconsider I9 = I as Subset of L2 by A1;

reconsider I9 = I9 as Ideal of L2 by A1, WAYBEL_0:3, WAYBEL_0:25;

I9 is prime

x is prime Ideal of L2 )

assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: for x being set st x is prime Ideal of L1 holds

x is prime Ideal of L2

let x be set ; :: thesis: ( x is prime Ideal of L1 implies x is prime Ideal of L2 )

assume x is prime Ideal of L1 ; :: thesis: x is prime Ideal of L2

then reconsider I = x as prime Ideal of L1 ;

reconsider I9 = I as Subset of L2 by A1;

reconsider I9 = I9 as Ideal of L2 by A1, WAYBEL_0:3, WAYBEL_0:25;

I9 is prime

proof

hence
x is prime Ideal of L2
; :: thesis: verum
let x, y be Element of L2; :: according to WAYBEL_7:def 1 :: thesis: ( not x "/\" y in I9 or x in I9 or y in I9 )

reconsider a = x, b = y as Element of L1 by A1;

A2: x "/\" y = inf {x,y} by YELLOW_0:40;

( ex_inf_of {a,b},L1 & a "/\" b = inf {a,b} ) by YELLOW_0:21, YELLOW_0:40;

then a "/\" b = x "/\" y by A1, A2, YELLOW_0:27;

hence ( not x "/\" y in I9 or x in I9 or y in I9 ) by Def1; :: thesis: verum

end;reconsider a = x, b = y as Element of L1 by A1;

A2: x "/\" y = inf {x,y} by YELLOW_0:40;

( ex_inf_of {a,b},L1 & a "/\" b = inf {a,b} ) by YELLOW_0:21, YELLOW_0:40;

then a "/\" b = x "/\" y by A1, A2, YELLOW_0:27;

hence ( not x "/\" y in I9 or x in I9 or y in I9 ) by Def1; :: thesis: verum