theorem :: WAYBEL_7:19

for L being LATTICE
for I being Ideal of L holds
( I is prime iff I in PRIME (InclPoset (Ids L)) )