E:(
), n,k:.
(EquivRel x,y:. x E y) 
((n E k) 
Min{ x | xEn } = Min{ x | xEk })
min_el_iff
})
Thm* E:(), n,k:.
(EquivRel x,y:. x E y) ((n E k) Min{ x | xEn } = Min{ x | xEk })
min_el_iff
Thm* E:(), n:. (EquivRel x,y:. x E y) (n E Min{ x | xEn })
min_el_sound
Thm* E:(), n,k:.
(EquivRel x,y:. x E y) (n E k) Min{ x | xEn } = Min{ x | xEk }
min_el_unique