(1) ( 的定义)
(2) (MP with 并集公理, A4)
(3) (有限交集)
(4) (MP with A4, 2)
(5) (MP with A4, 1)
(6) (Equv with 4, 5)
(7) (Equv with Ce, 6)
(8) (Equv with 量词可交换性 ,7)
(9) (E2)
(10) (AND)
(11) (D1 with 9,10)
(12)
(MP with A2, 11)
(13) (I)
(14) (MP with 12, 13)
(15) (AND)
(16) (D1 with 14,15)
(17) (GENe with then )
(18) (E1)
注意到配合(AND)和演绎定理有
(a)
(19) (a with 18)
(20) (A4)
(21) (MP with T, 20)
(22) (D1 with 19, 21)
(23) (GENe with )
(24) (AND with 17, 23)
(25) (Equv with 8, 24)
(26) (MP with A4, 3)
(27) (Equv with 25, 26)
(28) (Equv with Ce, 27)
(30) (MP with A4, 2)
(31) (Equv with 28, 30)
(32) (MP with A4, 3)
(33) (Equv with 31, 32)
(34) (GEN with , 33)
|