IsUFM(<ℤ+,*>)
{ ((BLemma `ufm_char` THENM RepD) THENA Auto) }
Cancel(|<ℤ+,*>|;|<ℤ+,*>|;*)
WellFnd{i}(|<ℤ+,*>|;x,y.x p| y)
1. a : Atom{<ℤ+,*>}@i
⊢ IsPrime(a)
1. a : |<ℤ+,*>|@i
⊢ Dec(Reducible(a))
2. b : |<ℤ+,*>|@i
⊢ Dec(a | b)