(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)
|