At: min el iff 2 1 1 1 1 1 1 1
1. E: 
2. n:
3. k:
4. Refl(;x,y.x E y)
5. 
a,b:. (a E b) 
(b E a)
6. a,b,c:. (a E b) (b E c) (a E c)
7. Min{ x | xEn } = Min{ x | xEk }
8. n E Min{ x | xEk }
9. k E Min{ x | xEk }
10. Min{ x | xEk } E k
n E k
By: FwdThru 6 [8;10]
Generated subgoals:None
About:
