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 Filter of L1 holds
x is prime Filter 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 Filter of L1 holds
x is prime Filter of L2
let x be set ; :: thesis: ( x is prime Filter of L1 implies x is prime Filter of L2 )
assume x is prime Filter of L1 ; :: thesis: x is prime Filter of L2
then reconsider I = x as prime Filter of L1 ;
reconsider I9 = I as Subset of L2 by A1;
reconsider I9 = I9 as Filter of L2 by A1, WAYBEL_0:4, WAYBEL_0:25;
I9 is prime
proof
let x, y be Element of L2; :: according to WAYBEL_7:def 2 :: 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 = sup {x,y} by YELLOW_0:41;
( ex_sup_of {a,b},L1 & a "\/" b = sup {a,b} ) by YELLOW_0:20, YELLOW_0:41;
then a "\/" b = x "\/" y by A1, A2, YELLOW_0:26;
hence ( not x "\/" y in I9 or x in I9 or y in I9 ) by Def2; :: thesis: verum
end;
hence x is prime Filter of L2 ; :: thesis: verum