:: Predicate Calculus for Boolean Valued Functions, II
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received March 13, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem :: BVFUNC_4:1
theorem :: BVFUNC_4:2
theorem :: BVFUNC_4:3
theorem :: BVFUNC_4:4
theorem Th5: :: BVFUNC_4:5
theorem :: BVFUNC_4:6
theorem Th7: :: BVFUNC_4:7
theorem Th8: :: BVFUNC_4:8
theorem :: BVFUNC_4:9
theorem Th10: :: BVFUNC_4:10
theorem :: BVFUNC_4:11
canceled;
theorem :: BVFUNC_4:12
theorem :: BVFUNC_4:13
theorem :: BVFUNC_4:14
theorem :: BVFUNC_4:15
theorem :: BVFUNC_4:16
theorem :: BVFUNC_4:17
theorem :: BVFUNC_4:18
theorem :: BVFUNC_4:19
theorem :: BVFUNC_4:20
theorem :: BVFUNC_4:21
theorem :: BVFUNC_4:22
theorem :: BVFUNC_4:23
theorem :: BVFUNC_4:24
theorem :: BVFUNC_4:25
theorem :: BVFUNC_4:26
theorem :: BVFUNC_4:27
theorem :: BVFUNC_4:28