:: Predicate Calculus for Boolean Valued Functions, { I } :: by Shunichi Kobayashi and Yatsuka Nakamura :: :: Received December 21, 1998 :: Copyright (c) 1998-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SUBSET_1, PARTIT1, MARGREL1, EQREL_1, BVFUNC_1, BVFUNC_2, XBOOLEAN, FUNCT_1; notations XBOOLE_0, SUBSET_1, XBOOLEAN, MARGREL1, FUNCT_2, EQREL_1, BVFUNC_1, BVFUNC_2; constructors BVFUNC_1, BVFUNC_2, RELSET_1, NUMBERS; registrations MARGREL1, ORDINAL1; requirements BOOLE, NUMERALS; definitions BVFUNC_1; equalities XBOOLEAN; expansions BVFUNC_1; theorems MARGREL1, BINARITH, BVFUNC_1, BVFUNC_2, XBOOLEAN, EQREL_1; begin :: Chap. 1 Predicate Calculus reserve Y for non empty set, G for Subset of PARTITIONS(Y), a,b,c,u for Function of Y,BOOLEAN, PA for a_partition of Y; theorem (a 'imp' b) '<' (All(a,PA,G) 'imp' Ex(b,PA,G)) proof let z be Element of Y; A1: ('not' a.z)=TRUE or ('not' a.z)=FALSE by XBOOLEAN:def 3; A2: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6; assume (a 'imp' b).z=TRUE; then A3: ('not' a.z) 'or' b.z=TRUE by BVFUNC_1:def 8; per cases by A3,A1,BINARITH:3; suppose 'not' a.z=TRUE; then a.z=FALSE by MARGREL1:11; then B_INF(a,CompF(PA,G)).z = FALSE by A2,BVFUNC_1:def 16; then All(a,PA,G).z=FALSE by BVFUNC_2:def 9; hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' FALSE) 'or' Ex(b,PA,G).z by BVFUNC_1:def 8 .=TRUE 'or' Ex(b,PA,G).z by MARGREL1:11 .=TRUE by BINARITH:10; end; suppose b.z=TRUE; then B_SUP(b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17; then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10; hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; end; theorem (All(a,PA,G) '&' All(b,PA,G)) '<' (a '&' b) proof let z be Element of Y; A1: (All(a,PA,G) '&' All(b,PA,G)).z =All(a,PA,G).z '&' All(b,PA,G).z by MARGREL1:def 20; assume A2: (All(a,PA,G) '&' All(b,PA,G)).z=TRUE; A3: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x=TRUE); then B_INF(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(a,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A2,A1,MARGREL1:12; end; A4: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6; now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x=TRUE); then B_INF(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(b,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A2,A1,MARGREL1:12; end; then A5: b.z=TRUE by A4; thus (a '&' b).z =a.z '&' b.z by MARGREL1:def 20 .=TRUE '&' TRUE by A4,A3,A5 .=TRUE; end; theorem (a '&' b) '<' (Ex(a,PA,G) '&' Ex(b,PA,G)) proof let z be Element of Y; A1: (a '&' b).z=a.z '&' b.z by MARGREL1:def 20; assume A2: (a '&' b).z=TRUE; then A3: Ex(a,PA,G) = B_SUP(a,CompF(PA,G)) & a.z=TRUE by A1,BVFUNC_2:def 10 ,MARGREL1:12; A4: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6; b.z=TRUE by A2,A1,MARGREL1:12; then B_SUP(b,CompF(PA,G)).z = TRUE by A4,BVFUNC_1:def 17; then A5: Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10; thus (Ex(a,PA,G) '&' Ex(b,PA,G)).z =Ex(a,PA,G).z '&' Ex(b,PA,G).z by MARGREL1:def 20 .=TRUE '&' TRUE by A3,A4,A5,BVFUNC_1:def 17 .=TRUE; end; theorem 'not' (All(a,PA,G) '&' All(b,PA,G)) = Ex('not' a,PA,G) 'or' Ex('not' b , PA, G ) proof A1: All(b,PA,G) = B_INF(b,CompF(PA,G)) by BVFUNC_2:def 9; A2: All(a,PA,G) = B_INF(a,CompF(PA,G)) by BVFUNC_2:def 9; A3: Ex('not' a,PA,G) 'or' Ex('not' b,PA,G) '<' 'not' (All(a,PA,G) '&' All(b ,PA,G)) proof let z be Element of Y; A4: (Ex('not' a,PA,G) 'or' Ex('not' b,PA,G)).z =Ex('not' a,PA,G).z 'or' Ex('not' b,PA,G).z by BVFUNC_1:def 4; A5: Ex('not' b,PA,G).z=TRUE or Ex('not' b,PA,G).z=FALSE by XBOOLEAN:def 3; assume A6: (Ex('not' a,PA,G) 'or' Ex('not' b,PA,G)).z=TRUE; per cases by A6,A4,A5,BINARITH:3; suppose A7: Ex('not' a,PA,G).z=TRUE; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & ('not' a).x=TRUE); then B_SUP('not' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; hence contradiction by A7,BVFUNC_2:def 10; end; then consider x1 being Element of Y such that A8: x1 in EqClass(z,CompF(PA,G)) and A9: ('not' a).x1=TRUE; 'not' a.x1=TRUE by A9,MARGREL1:def 19; then A10: a.x1=FALSE by MARGREL1:11; thus ('not' (All(a,PA,G) '&' All(b,PA,G))).z ='not' ((All(a,PA,G) '&' All(b,PA,G))).z by MARGREL1:def 19 .='not' (All(a,PA,G).z '&' All(b,PA,G).z) by MARGREL1:def 20 .='not' (FALSE '&' All(b,PA,G).z) by A2,A8,A10,BVFUNC_1:def 16 .='not' (FALSE) by MARGREL1:12 .=TRUE by MARGREL1:11; end; suppose A11: Ex('not' b,PA,G).z=TRUE; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & ('not' b).x=TRUE); then B_SUP('not' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; hence contradiction by A11,BVFUNC_2:def 10; end; then consider x1 being Element of Y such that A12: x1 in EqClass(z,CompF(PA,G)) and A13: ('not' b).x1=TRUE; 'not' b.x1=TRUE by A13,MARGREL1:def 19; then A14: b.x1=FALSE by MARGREL1:11; thus ('not' (All(a,PA,G) '&' All(b,PA,G))).z ='not' ((All(a,PA,G) '&' All(b,PA,G))).z by MARGREL1:def 19 .='not' (All(a,PA,G).z '&' All(b,PA,G).z) by MARGREL1:def 20 .='not' (All(a,PA,G).z '&' FALSE) by A1,A12,A14,BVFUNC_1:def 16 .='not' (FALSE) by MARGREL1:12 .=TRUE by MARGREL1:11; end; end; 'not' (All(a,PA,G) '&' All(b,PA,G)) '<' (Ex('not' a,PA,G) 'or' Ex('not' b,PA,G)) proof let z be Element of Y; assume ('not' (All(a,PA,G) '&' All(b,PA,G))).z=TRUE; then A15: 'not' ((All(a,PA,G) '&' All(b,PA,G))).z=TRUE by MARGREL1:def 19; (All(a,PA,G) '&' All(b,PA,G)).z =All(a,PA,G).z '&' All(b,PA,G).z by MARGREL1:def 20; then A16: All(a,PA,G).z '&' All(b,PA,G).z=FALSE by A15,MARGREL1:11; per cases by A16,MARGREL1:12; suppose All(a,PA,G).z=FALSE; then consider x1 being Element of Y such that A17: x1 in EqClass(z,CompF(PA,G)) and A18: a.x1<>TRUE by A2,BVFUNC_1:def 16; a.x1=FALSE by A18,XBOOLEAN:def 3; then 'not' a.x1=TRUE by MARGREL1:11; then ('not' a).x1=TRUE by MARGREL1:def 19; then B_SUP('not' a,CompF(PA,G)).z = TRUE by A17,BVFUNC_1:def 17; then Ex('not' a,PA,G).z =TRUE by BVFUNC_2:def 10; hence (Ex('not' a,PA,G) 'or' Ex('not' b,PA,G)).z =TRUE 'or' Ex('not' b,PA ,G).z by BVFUNC_1:def 4 .=TRUE by BINARITH:10; end; suppose All(b,PA,G).z=FALSE; then consider x1 being Element of Y such that A19: x1 in EqClass(z,CompF(PA,G)) and A20: b.x1<>TRUE by A1,BVFUNC_1:def 16; b.x1=FALSE by A20,XBOOLEAN:def 3; then 'not' b.x1=TRUE by MARGREL1:11; then ('not' b).x1=TRUE by MARGREL1:def 19; then B_SUP('not' b,CompF(PA,G)).z = TRUE by A19,BVFUNC_1:def 17; then Ex('not' b,PA,G).z =TRUE by BVFUNC_2:def 10; hence (Ex('not' a,PA,G) 'or' Ex('not' b,PA,G)).z =Ex('not' a,PA,G).z 'or' TRUE by BVFUNC_1:def 4 .=TRUE by BINARITH:10; end; end; hence thesis by A3,BVFUNC_1:15; end; theorem 'not' (Ex(a,PA,G) '&' Ex(b,PA,G)) = All('not' a,PA,G) 'or' All('not' b ,PA,G) proof A1: All('not' b,PA,G) = B_INF('not' b,CompF(PA,G)) by BVFUNC_2:def 9; A2: Ex(b,PA,G) = B_SUP(b,CompF(PA,G)) by BVFUNC_2:def 10; A3: Ex(a,PA,G) = B_SUP(a,CompF(PA,G)) by BVFUNC_2:def 10; A4: All('not' a,PA,G) 'or' All('not' b,PA,G) '<' 'not' (Ex(a,PA,G) '&' Ex(b ,PA,G)) proof let z be Element of Y; A5: All('not' b,PA,G).z=TRUE or All('not' b,PA,G).z=FALSE by XBOOLEAN:def 3; assume (All('not' a,PA,G) 'or' All('not' b,PA,G)) .z=TRUE; then A6: All('not' a,PA,G).z 'or' All('not' b,PA,G).z=TRUE by BVFUNC_1:def 4; per cases by A6,A5,BINARITH:3; suppose A7: All('not' a,PA,G).z=TRUE; A8: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds ('not' a).x=TRUE); then B_INF('not' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; hence contradiction by A7,BVFUNC_2:def 9; end; A9: now let x be Element of Y; assume x in EqClass(z,CompF(PA,G)); then ('not' a).x=TRUE by A8; then 'not' a.x=TRUE by MARGREL1:def 19; hence a.x<>TRUE by MARGREL1:11; end; thus ('not' (Ex(a,PA,G) '&' Ex(b,PA,G))).z ='not' (Ex(a,PA,G) '&' Ex(b, PA,G)).z by MARGREL1:def 19 .='not' (Ex(a,PA,G).z '&' Ex(b,PA,G).z) by MARGREL1:def 20 .='not' (FALSE '&' Ex(b,PA,G).z) by A3,A9,BVFUNC_1:def 17 .='not' (FALSE) by MARGREL1:12 .=TRUE by MARGREL1:11; end; suppose A10: All('not' b,PA,G).z=TRUE; A11: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds ('not' b).x=TRUE); then B_INF('not' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; hence contradiction by A10,BVFUNC_2:def 9; end; A12: now let x be Element of Y; assume x in EqClass(z,CompF(PA,G)); then ('not' b).x=TRUE by A11; then 'not' b.x=TRUE by MARGREL1:def 19; hence b.x<>TRUE by MARGREL1:11; end; thus ('not' (Ex(a,PA,G) '&' Ex(b,PA,G))).z ='not' (Ex(a,PA,G) '&' Ex(b, PA,G)).z by MARGREL1:def 19 .='not' (Ex(a,PA,G).z '&' Ex(b,PA,G).z) by MARGREL1:def 20 .='not' (Ex(a,PA,G).z '&' FALSE) by A2,A12,BVFUNC_1:def 17 .='not' (FALSE) by MARGREL1:12 .=TRUE by MARGREL1:11; end; end; A13: All('not' a,PA,G) = B_INF('not' a,CompF(PA,G)) by BVFUNC_2:def 9; 'not' (Ex(a,PA,G) '&' Ex(b,PA,G)) '<' (All('not' a,PA,G) 'or' All('not' b,PA,G)) proof let z be Element of Y; assume ('not' (Ex(a,PA,G) '&' Ex(b,PA,G))).z=TRUE; then 'not' (Ex(a,PA,G) '&' Ex(b,PA,G)).z=TRUE by MARGREL1:def 19; then (Ex(a,PA,G) '&' Ex(b,PA,G)).z=FALSE by MARGREL1:11; then A14: Ex(a,PA,G).z '&' Ex(b,PA,G).z=FALSE by MARGREL1:def 20; per cases by A14,MARGREL1:12; suppose A15: Ex(a,PA,G).z=FALSE; A16: now let x be Element of Y; assume x in EqClass(z,CompF(PA,G)); then a.x<>TRUE by A3,A15,BVFUNC_1:def 17; then a.x=FALSE by XBOOLEAN:def 3; then 'not' a.x=TRUE by MARGREL1:11; hence ('not' a).x=TRUE by MARGREL1:def 19; end; thus (All('not' a,PA,G) 'or' All('not' b,PA,G)) .z = All('not' a,PA,G).z 'or' All('not' b,PA,G).z by BVFUNC_1:def 4 .= TRUE 'or' All('not' b,PA,G).z by A13,A16,BVFUNC_1:def 16 .= TRUE by BINARITH:10; end; suppose A17: Ex(b,PA,G).z=FALSE; A18: now let x be Element of Y; assume x in EqClass(z,CompF(PA,G)); then b.x<>TRUE by A2,A17,BVFUNC_1:def 17; then b.x=FALSE by XBOOLEAN:def 3; then 'not' b.x=TRUE by MARGREL1:11; hence ('not' b).x=TRUE by MARGREL1:def 19; end; thus (All('not' a,PA,G) 'or' All('not' b,PA,G)) .z = All('not' a,PA,G).z 'or' All('not' b,PA,G).z by BVFUNC_1:def 4 .= All('not' a,PA,G).z 'or' TRUE by A1,A18,BVFUNC_1:def 16 .= TRUE by BINARITH:10; end; end; hence thesis by A4,BVFUNC_1:15; end; theorem (All(a,PA,G) 'or' All(b,PA,G)) '<' (a 'or' b) proof let z be Element of Y; A1: All(a,PA,G).z=TRUE or All(a,PA,G).z=FALSE by XBOOLEAN:def 3; A2: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6; assume (All(a,PA,G) 'or' All(b,PA,G)) .z=TRUE; then A3: All(a,PA,G).z 'or' All(b,PA,G).z=TRUE by BVFUNC_1:def 4; per cases by A3,A1,BINARITH:3; suppose A4: All(a,PA,G).z=TRUE; A5: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x=TRUE); then B_INF(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; hence contradiction by A4,BVFUNC_2:def 9; end; thus (a 'or' b).z = a.z 'or' b.z by BVFUNC_1:def 4 .= TRUE 'or' b.z by A2,A5 .= TRUE by BINARITH:10; end; suppose A6: All(b,PA,G).z=TRUE; A7: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x=TRUE); then B_INF(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; hence contradiction by A6,BVFUNC_2:def 9; end; thus (a 'or' b).z = a.z 'or' b.z by BVFUNC_1:def 4 .= a.z 'or' TRUE by A2,A7 .= TRUE by BINARITH:10; end; end; theorem (a 'or' b) '<' (Ex(a,PA,G) 'or' Ex(b,PA,G)) proof A1: Ex(a,PA,G) = B_SUP(a,CompF(PA,G)) by BVFUNC_2:def 10; let z be Element of Y; A2: Ex(b,PA,G) = B_SUP(b,CompF(PA,G)) by BVFUNC_2:def 10; A3: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6; assume (a 'or' b).z=TRUE; then A4: a.z 'or' b.z=TRUE by BVFUNC_1:def 4; A5: b.z=TRUE or b.z=FALSE by XBOOLEAN:def 3; per cases by A4,A5,BINARITH:3; suppose A6: a.z=TRUE; thus (Ex(a,PA,G) 'or' Ex(b,PA,G)).z =Ex(a,PA,G).z 'or' Ex(b,PA,G).z by BVFUNC_1:def 4 .=TRUE 'or' Ex(b,PA,G).z by A1,A3,A6,BVFUNC_1:def 17 .=TRUE by BINARITH:10; end; suppose A7: b.z=TRUE; thus (Ex(a,PA,G) 'or' Ex(b,PA,G)).z =Ex(a,PA,G).z 'or' Ex(b,PA,G).z by BVFUNC_1:def 4 .=Ex(a,PA,G).z 'or' TRUE by A2,A3,A7,BVFUNC_1:def 17 .=TRUE by BINARITH:10; end; end; theorem (a 'xor' b) '<' ('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)) 'or' 'not' (Ex(a,PA,G) 'xor' Ex( 'not' b,PA,G))) proof A1: Ex('not' a,PA,G) = B_SUP('not' a,CompF(PA,G)) by BVFUNC_2:def 10; let z be Element of Y; A2: Ex('not' b,PA,G) = B_SUP('not' b,CompF(PA,G)) by BVFUNC_2:def 10; A3: (a.z '&' 'not' b.z)=TRUE or (a.z '&' 'not' b.z)=FALSE by XBOOLEAN:def 3; A4: (a 'xor' b).z =a.z 'xor' b.z by BVFUNC_1:def 5 .=('not' a.z '&' b.z) 'or' (a.z '&' 'not' b.z); A5: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6; A6: FALSE '&' TRUE =FALSE by MARGREL1:13; assume A7: (a 'xor' b).z=TRUE; per cases by A7,A4,A3,BINARITH:3; suppose A8: ('not' a.z '&' b.z)=TRUE; then 'not' a.z=TRUE by MARGREL1:12; then ('not' a).z=TRUE by MARGREL1:def 19; then A9: B_SUP('not' a,CompF(PA,G)).z = TRUE by A5,BVFUNC_1:def 17; A10: ('not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z ='not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G)).z by MARGREL1:def 19; b.z=TRUE by A8,MARGREL1:12; then B_SUP(b,CompF(PA,G)).z = TRUE by A5,BVFUNC_1:def 17; then A11: Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10; A12: (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)).z =Ex('not' a,PA,G).z 'xor' Ex(b, PA,G).z by BVFUNC_1:def 5 .=FALSE by A1,A6,A9,A11,MARGREL1:11; thus ('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)) 'or' 'not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z =('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G))).z 'or' ('not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z by BVFUNC_1:def 4 .='not' FALSE 'or' 'not' ((Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z by A12 ,A10,MARGREL1:def 19 .=TRUE 'or' 'not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G)).z by MARGREL1:11 .=TRUE by BINARITH:10; end; suppose A13: (a.z '&' 'not' b.z)=TRUE; then a.z=TRUE by MARGREL1:12; then B_SUP(a,CompF(PA,G)).z = TRUE by A5,BVFUNC_1:def 17; then A14: Ex(a,PA,G).z=TRUE by BVFUNC_2:def 10; A15: ('not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z ='not' ((Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z by MARGREL1:def 19; 'not' b.z=TRUE by A13,MARGREL1:12; then ('not' b).z=TRUE by MARGREL1:def 19; then A16: B_SUP('not' b,CompF(PA,G)).z = TRUE by A5,BVFUNC_1:def 17; A17: (Ex(a,PA,G) 'xor' Ex('not' b,PA,G)).z =Ex(a,PA,G).z 'xor' Ex('not' b, PA,G).z by BVFUNC_1:def 5 .=FALSE by A2,A6,A16,A14,MARGREL1:11; thus ('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)) 'or' 'not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z =('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G))).z 'or' ('not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z by BVFUNC_1:def 4 .='not' ((Ex('not' a,PA,G) 'xor' Ex(b,PA,G))).z 'or' 'not' FALSE by A17 ,A15,MARGREL1:def 19 .='not' ((Ex('not' a,PA,G) 'xor' Ex(b,PA,G))).z 'or' TRUE by MARGREL1:11 .=TRUE by BINARITH:10; end; end; theorem All(a 'or' b,PA,G) '<' All(a,PA,G) 'or' Ex(b,PA,G) proof let z be Element of Y; assume A1: All(a 'or' b,PA,G).z=TRUE; A2: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'or' b).x=TRUE); then B_INF(a 'or' b,CompF(PA,G)).z=FALSE by BVFUNC_1:def 16; hence contradiction by A1,BVFUNC_2:def 9; end; per cases; suppose ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE; then B_SUP(b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17; then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10; hence (All(a,PA,G) 'or' Ex(b,PA,G)) .z =All(a,PA,G).z 'or' TRUE by BVFUNC_1:def 4 .=TRUE by BINARITH:10; end; suppose (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a. x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x= TRUE); then B_INF(a,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16; then All(a,PA,G).z=TRUE by BVFUNC_2:def 9; hence (All(a,PA,G) 'or' Ex(b,PA,G)) .z =TRUE 'or' Ex(b,PA,G).z by BVFUNC_1:def 4 .=TRUE by BINARITH:10; end; suppose A3: not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE); then consider x1 being Element of Y such that A4: x1 in EqClass(z,CompF(PA,G)) and A5: a.x1<>TRUE; A6: b.x1<>TRUE by A3,A4; A7: a.x1=FALSE by A5,XBOOLEAN:def 3; (a 'or' b).x1 = a.x1 'or' b.x1 by BVFUNC_1:def 4 .= FALSE 'or' FALSE by A6,A7,XBOOLEAN:def 3 .= FALSE; hence thesis by A2,A4; end; end; Lm1: now let Y,a,b,G,PA; let z be Element of Y; assume A1: All(a 'or' b,PA,G).z=TRUE; assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds ( a 'or' b).x=TRUE); then B_INF(a 'or' b,CompF(PA,G)).z=FALSE by BVFUNC_1:def 16; hence contradiction by A1,BVFUNC_2:def 9; end; theorem All(a 'or' b,PA,G) '<' Ex(a,PA,G) 'or' All(b,PA,G) proof let z be Element of Y; assume A1: All(a 'or' b,PA,G).z=TRUE; per cases; suppose ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x=TRUE; then B_SUP(a,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17; then Ex(a,PA,G).z=TRUE by BVFUNC_2:def 10; hence (Ex(a,PA,G) 'or' All(b,PA,G)) .z = TRUE 'or' All(b,PA,G).z by BVFUNC_1:def 4 .=TRUE by BINARITH:10; end; suppose (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x =TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x=TRUE ); then B_INF(b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16; then All(b,PA,G).z=TRUE by BVFUNC_2:def 9; hence (Ex(a,PA,G) 'or' All(b,PA,G)) .z =Ex(a,PA,G).z 'or' TRUE by BVFUNC_1:def 4 .=TRUE by BINARITH:10; end; suppose A2: not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x=TRUE); then consider x1 being Element of Y such that A3: x1 in EqClass(z,CompF(PA,G)) and A4: b.x1<>TRUE; A5: a.x1<>TRUE by A2,A3; A6: b.x1=FALSE by A4,XBOOLEAN:def 3; (a 'or' b).x1 = a.x1 'or' b.x1 by BVFUNC_1:def 4 .= FALSE 'or' FALSE by A5,A6,XBOOLEAN:def 3 .= FALSE; hence thesis by A1,A3,Lm1; end; end; theorem All(a 'or' b,PA,G) '<' Ex(a,PA,G) 'or' Ex(b,PA,G) proof let z be Element of Y; A1: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6; assume All(a 'or' b,PA,G).z=TRUE; then (a 'or' b).z=TRUE by A1,Lm1; then A2: a.z 'or' b.z=TRUE by BVFUNC_1:def 4; A3: a.z=TRUE or a.z=FALSE by XBOOLEAN:def 3; per cases by A2,A3,BINARITH:3; suppose a.z=TRUE; then B_SUP(a,CompF(PA,G)).z = TRUE by A1,BVFUNC_1:def 17; then Ex(a,PA,G).z=TRUE by BVFUNC_2:def 10; hence (Ex(a,PA,G) 'or' Ex(b,PA,G)).z =TRUE 'or' Ex(b,PA,G).z by BVFUNC_1:def 4 .=TRUE by BINARITH:10; end; suppose b.z=TRUE; then B_SUP(b,CompF(PA,G)).z = TRUE by A1,BVFUNC_1:def 17; then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10; hence (Ex(a,PA,G) 'or' Ex(b,PA,G)).z =Ex(a,PA,G).z 'or' TRUE by BVFUNC_1:def 4 .=TRUE by BINARITH:10; end; end; theorem Ex(a,PA,G) '&' All(b,PA,G) '<' Ex(a '&' b,PA,G) proof let z be Element of Y; assume (Ex(a,PA,G) '&' All(b,PA,G)) .z=TRUE; then A1: Ex(a,PA,G).z '&' All(b,PA,G).z=TRUE by MARGREL1:def 20; A2: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x=TRUE); then B_INF(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(b,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x= TRUE); then B_SUP(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; then Ex(a,PA,G).z=FALSE by BVFUNC_2:def 10; hence contradiction by A1,MARGREL1:12; end; then consider x1 being Element of Y such that A3: x1 in EqClass(z,CompF(PA,G)) and A4: a.x1=TRUE; (a '&' b).x1 =a.x1 '&' b.x1 by MARGREL1:def 20 .=TRUE '&' TRUE by A3,A4,A2 .=TRUE; then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A3,BVFUNC_1:def 17; hence thesis by BVFUNC_2:def 10; end; theorem All(a,PA,G) '&' Ex(b,PA,G) '<' Ex(a '&' b,PA,G) proof let z be Element of Y; assume (All(a,PA,G) '&' Ex(b,PA,G)) .z=TRUE; then A1: All(a,PA,G).z '&' Ex(b,PA,G).z=TRUE by MARGREL1:def 20; A2: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x=TRUE); then B_INF(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(a,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x= TRUE); then B_SUP(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; then Ex(b,PA,G).z=FALSE by BVFUNC_2:def 10; hence contradiction by A1,MARGREL1:12; end; then consider x1 being Element of Y such that A3: x1 in EqClass(z,CompF(PA,G)) and A4: b.x1=TRUE; (a '&' b).x1 =a.x1 '&' b.x1 by MARGREL1:def 20 .=TRUE '&' TRUE by A3,A4,A2 .=TRUE; then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A3,BVFUNC_1:def 17; hence thesis by BVFUNC_2:def 10; end; Lm2: now let Y,a,b,G,PA; let z be Element of Y; assume A1: All(a 'imp' b,PA,G).z=TRUE; assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds ( a 'imp' b).x=TRUE); then B_INF(a 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; hence contradiction by A1,BVFUNC_2:def 9; end; theorem All(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G) proof A1: All(a,PA,G) = B_INF(a,CompF(PA,G)) by BVFUNC_2:def 9; let z be Element of Y; assume A2: All(a 'imp' b,PA,G).z=TRUE; A3: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6; per cases; suppose ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE; then B_SUP(b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17; then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10; hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x =TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE ); then A4: b.z<>TRUE & a.z=TRUE by A3; (a 'imp' b).z =('not' a.z) 'or' b.z by BVFUNC_1:def 8 .=('not' TRUE) 'or' FALSE by A4,XBOOLEAN:def 3 .=FALSE 'or' FALSE by MARGREL1:11 .=FALSE; hence thesis by A2,A3,Lm2; end; suppose A5: not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE); thus (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' Ex(b,PA, G).z by BVFUNC_1:def 8 .=('not' FALSE) 'or' Ex(b,PA,G).z by A1,A5,BVFUNC_1:def 16 .=TRUE 'or' Ex(b,PA,G).z by MARGREL1:11 .=TRUE by BINARITH:10; end; end; theorem All(a 'imp' b,PA,G) '<' Ex(a,PA,G) 'imp' Ex(b,PA,G) proof A1: Ex(a,PA,G) = B_SUP(a,CompF(PA,G)) by BVFUNC_2:def 10; let z be Element of Y; assume A2: All(a 'imp' b,PA,G).z=TRUE; per cases; suppose ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE; then B_SUP(b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17; then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10; hence (Ex(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' Ex(a,PA,G).z) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose A3: (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x=TRUE ) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE); then consider x1 being Element of Y such that A4: x1 in EqClass(z,CompF(PA,G)) and A5: a.x1=TRUE; A6: b.x1<>TRUE by A3,A4; (a 'imp' b).x1 =('not' a.x1) 'or' b.x1 by BVFUNC_1:def 8 .=('not' TRUE) 'or' FALSE by A5,A6,XBOOLEAN:def 3 .=FALSE 'or' FALSE by MARGREL1:11 .=FALSE; hence thesis by A2,A4,Lm2; end; suppose A7: not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x =TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE ); thus (Ex(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' Ex(a,PA,G).z) 'or' Ex(b,PA,G) .z by BVFUNC_1:def 8 .=('not' FALSE) 'or' Ex(b,PA,G).z by A1,A7,BVFUNC_1:def 17 .=TRUE 'or' Ex(b,PA,G).z by MARGREL1:11 .=TRUE by BINARITH:10; end; end; theorem Ex(a,PA,G) 'imp' All(b,PA,G) '<' All(a 'imp' b,PA,G) proof let z be Element of Y; assume (Ex(a,PA,G) 'imp' All(b,PA,G)).z=TRUE; then A1: ('not' Ex(a,PA,G).z) 'or' All(b,PA,G).z=TRUE by BVFUNC_1:def 8; per cases; suppose A2: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x= TRUE; for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp' b).x=TRUE proof let x be Element of Y; assume A3: x in EqClass(z,CompF(PA,G)); thus (a 'imp' b).x=('not' a.x) 'or' b.x by BVFUNC_1:def 8 .=('not' a.x) 'or' TRUE by A2,A3 .=TRUE by BINARITH:10; end; then B_INF(a 'imp' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16; hence thesis by BVFUNC_2:def 9; end; suppose A4: (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x=TRUE ) & not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x=TRUE ); then B_SUP(a,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17; then Ex(a,PA,G).z=TRUE by BVFUNC_2:def 10; then A5: 'not' Ex(a,PA,G).z=FALSE by MARGREL1:11; B_INF(b,CompF(PA,G)).z = FALSE by A4,BVFUNC_1:def 16; then All(b,PA,G).z=FALSE by BVFUNC_2:def 9; hence thesis by A1,A5; end; suppose A6: not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x =TRUE) & not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x =TRUE); now let x be Element of Y; assume x in EqClass(z,CompF(PA,G)); then A7: a.x<>TRUE by A6; thus (a 'imp' b).x =('not' a.x) 'or' b.x by BVFUNC_1:def 8 .=('not' FALSE) 'or' b.x by A7,XBOOLEAN:def 3 .=TRUE 'or' b.x by MARGREL1:11 .=TRUE by BINARITH:10; end; then B_INF(a 'imp' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16; hence thesis by BVFUNC_2:def 9; end; end; theorem (a 'imp' b) '<' (a 'imp' Ex(b,PA,G)) proof let z be Element of Y; A1: ('not' a.z)=TRUE or ('not' a.z)=FALSE by XBOOLEAN:def 3; A2: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6; assume (a 'imp' b).z=TRUE; then A3: ('not' a.z) 'or' b.z=TRUE by BVFUNC_1:def 8; per cases by A3,A1,BINARITH:3; suppose 'not' a.z=TRUE; hence (a 'imp' Ex(b,PA,G)).z =TRUE 'or' Ex(b,PA,G).z by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose b.z=TRUE; then B_SUP(b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17; then Ex(b,PA,G).z =TRUE by BVFUNC_2:def 10; hence (a 'imp' Ex(b,PA,G)).z =('not' a.z) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; end; theorem (a 'imp' b) '<' (All(a,PA,G) 'imp' b) proof let z be Element of Y; A1: ('not' a.z)=TRUE or ('not' a.z)=FALSE by XBOOLEAN:def 3; A2: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6; assume (a 'imp' b).z=TRUE; then A3: ('not' a.z) 'or' b.z=TRUE by BVFUNC_1:def 8; per cases by A3,A1,BINARITH:3; suppose 'not' a.z=TRUE; then a.z=FALSE by MARGREL1:11; then B_INF(a,CompF(PA,G)).z = FALSE by A2,BVFUNC_1:def 16; then All(a,PA,G).z=FALSE by BVFUNC_2:def 9; hence (All(a,PA,G) 'imp' b).z =('not' FALSE) 'or' b.z by BVFUNC_1:def 8 .=TRUE 'or' b.z by MARGREL1:11 .=TRUE by BINARITH:10; end; suppose b.z=TRUE; hence (All(a,PA,G) 'imp' b).z =('not' All(a,PA,G).z) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; end; theorem Ex(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G) proof let z be Element of Y; assume A1: Ex(a 'imp' b,PA,G).z=TRUE; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & (a 'imp' b).x=TRUE); then B_SUP(a 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; hence contradiction by A1,BVFUNC_2:def 10; end; then consider x1 being Element of Y such that A2: x1 in EqClass(z,CompF(PA,G)) and A3: (a 'imp' b).x1=TRUE; A4: ('not' a.x1) 'or' b.x1=TRUE by A3,BVFUNC_1:def 8; A5: b.x1=TRUE or b.x1=FALSE by XBOOLEAN:def 3; per cases by A4,A5,BINARITH:3; suppose ('not' a.x1)=TRUE; then a.x1=FALSE by MARGREL1:11; then B_INF(a,CompF(PA,G)).z = FALSE by A2,BVFUNC_1:def 16; then All(a,PA,G).z=FALSE by BVFUNC_2:def 9; hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' FALSE) 'or' Ex(b,PA,G).z by BVFUNC_1:def 8 .=TRUE 'or' Ex(b,PA,G).z by MARGREL1:11 .=TRUE by BINARITH:10; end; suppose b.x1=TRUE; then B_SUP(b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17; then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10; hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; end; theorem All(a,PA,G) '<' Ex(b,PA,G) 'imp' Ex(a '&' b,PA,G) proof let z be Element of Y; assume A1: All(a,PA,G).z=TRUE; A2: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x=TRUE); then B_INF(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; hence contradiction by A1,BVFUNC_2:def 9; end; per cases; suppose A3: Ex(b,PA,G).z=TRUE; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b. x=TRUE); then B_SUP(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; hence contradiction by A3,BVFUNC_2:def 10; end; then consider x1 being Element of Y such that A4: x1 in EqClass(z,CompF(PA,G)) and A5: b.x1=TRUE; (a '&' b).x1 =a.x1 '&' b.x1 by MARGREL1:def 20 .=TRUE '&' TRUE by A2,A4,A5 .=TRUE; then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A4,BVFUNC_1:def 17; then Ex(a '&' b,PA,G).z=TRUE by BVFUNC_2:def 10; hence (Ex(b,PA,G) 'imp' Ex(a '&' b,PA,G)).z =('not' Ex(b,PA,G).z) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose Ex(b,PA,G).z<>TRUE; then Ex(b,PA,G).z=FALSE by XBOOLEAN:def 3; hence (Ex(b,PA,G) 'imp' Ex(a '&' b,PA,G)).z =('not' FALSE) 'or' Ex(a '&' b, PA,G).z by BVFUNC_1:def 8 .=TRUE 'or' Ex(a '&' b,PA,G).z by MARGREL1:11 .=TRUE by BINARITH:10; end; end; theorem u is_independent_of PA,G implies Ex(u 'imp' a,PA,G) '<' (u 'imp' Ex(a, PA,G)) proof assume u is_independent_of PA,G; then A1: u is_dependent_of CompF(PA,G) by BVFUNC_2:def 8; let z be Element of Y; A2: z in EqClass(z,CompF(PA,G)) & EqClass(z,CompF(PA,G)) in CompF(PA,G) by EQREL_1:def 6; assume A3: Ex(u 'imp' a,PA,G).z=TRUE; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & (u 'imp' a).x=TRUE); then B_SUP(u 'imp' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; hence contradiction by A3,BVFUNC_2:def 10; end; then consider x1 being Element of Y such that A4: x1 in EqClass(z,CompF(PA,G)) and A5: (u 'imp' a).x1=TRUE; A6: ('not' u.x1) 'or' a.x1=TRUE by A5,BVFUNC_1:def 8; A7: ('not' u.x1)=TRUE or ('not' u.x1)=FALSE by XBOOLEAN:def 3; per cases by A6,A7,BINARITH:3; suppose A8: ('not' u.x1)=TRUE; u.x1 = u.z by A1,A4,A2; then u.z=FALSE by A8,MARGREL1:11; hence (u 'imp' Ex(a,PA,G)).z =('not' FALSE) 'or' Ex(a,PA,G).z by BVFUNC_1:def 8 .=TRUE 'or' Ex(a,PA,G).z by MARGREL1:11 .=TRUE by BINARITH:10; end; suppose a.x1=TRUE; then B_SUP(a,CompF(PA,G)).z = TRUE by A4,BVFUNC_1:def 17; then Ex(a,PA,G).z=TRUE by BVFUNC_2:def 10; hence (u 'imp' Ex(a,PA,G)).z =('not' u.z) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; end; theorem u is_independent_of PA,G implies Ex(a 'imp' u,PA,G) '<' (All(a,PA,G) 'imp' u) proof assume u is_independent_of PA,G; then A1: u is_dependent_of CompF(PA,G) by BVFUNC_2:def 8; let z be Element of Y; A2: z in EqClass(z,CompF(PA,G)) & EqClass(z,CompF(PA,G)) in CompF(PA,G) by EQREL_1:def 6; assume A3: Ex(a 'imp' u,PA,G).z=TRUE; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & (a 'imp' u).x=TRUE); then B_SUP(a 'imp' u,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; hence contradiction by A3,BVFUNC_2:def 10; end; then consider x1 being Element of Y such that A4: x1 in EqClass(z,CompF(PA,G)) and A5: (a 'imp' u).x1=TRUE; A6: ('not' a.x1) 'or' u.x1=TRUE by A5,BVFUNC_1:def 8; A7: ('not' a.x1)=TRUE or ('not' a.x1)=FALSE by XBOOLEAN:def 3; per cases by A6,A7,BINARITH:3; suppose ('not' a.x1)=TRUE; then a.x1=FALSE by MARGREL1:11; then B_INF(a,CompF(PA,G)).z = FALSE by A4,BVFUNC_1:def 16; then All(a,PA,G).z=FALSE by BVFUNC_2:def 9; hence (All(a,PA,G) 'imp' u).z =('not' FALSE) 'or' u.z by BVFUNC_1:def 8 .=TRUE 'or' u.z by MARGREL1:11 .=TRUE by BINARITH:10; end; suppose A8: u.x1=TRUE; u.x1 = u.z by A1,A4,A2; hence (All(a,PA,G) 'imp' u).z =('not' All(a,PA,G).z) 'or' TRUE by A8, BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; end; theorem All(a,PA,G) 'imp' Ex(b,PA,G) = Ex(a 'imp' b,PA,G) proof A1: All(a,PA,G) = B_INF(a,CompF(PA,G)) by BVFUNC_2:def 9; A2: All(a,PA,G) 'imp' Ex(b,PA,G) '<' Ex(a 'imp' b,PA,G) proof let z be Element of Y; A3: ('not' All(a,PA,G).z)=TRUE or ('not' All(a,PA,G).z)=FALSE by XBOOLEAN:def 3 ; assume (All(a,PA,G) 'imp' Ex(b,PA,G)).z=TRUE; then A4: ('not' All(a,PA,G).z) 'or' Ex(b,PA,G).z=TRUE by BVFUNC_1:def 8; per cases by A4,A3,BINARITH:3; suppose ('not' All(a,PA,G).z)=TRUE; then All(a,PA,G).z=FALSE by MARGREL1:11; then consider x1 being Element of Y such that A5: x1 in EqClass(z,CompF(PA,G)) and A6: a.x1<>TRUE by A1,BVFUNC_1:def 16; (a 'imp' b).x1 =('not' a.x1) 'or' b.x1 by BVFUNC_1:def 8 .=('not' FALSE) 'or' b.x1 by A6,XBOOLEAN:def 3 .=TRUE 'or' b.x1 by MARGREL1:11 .=TRUE by BINARITH:10; then B_SUP(a 'imp' b,CompF(PA,G)).z = TRUE by A5,BVFUNC_1:def 17; hence thesis by BVFUNC_2:def 10; end; suppose A7: Ex(b,PA,G).z=TRUE; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE); then B_SUP(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; hence contradiction by A7,BVFUNC_2:def 10; end; then consider x1 being Element of Y such that A8: x1 in EqClass(z,CompF(PA,G)) and A9: b.x1=TRUE; (a 'imp' b).x1 =('not' a.x1) 'or' TRUE by A9,BVFUNC_1:def 8 .=TRUE by BINARITH:10; then B_SUP(a 'imp' b,CompF(PA,G)).z = TRUE by A8,BVFUNC_1:def 17; hence thesis by BVFUNC_2:def 10; end; end; Ex(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G) proof let z be Element of Y; assume A10: Ex(a 'imp' b,PA,G).z=TRUE; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & ( a 'imp' b).x=TRUE); then B_SUP(a 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; hence contradiction by A10,BVFUNC_2:def 10; end; then consider x1 being Element of Y such that A11: x1 in EqClass(z,CompF(PA,G)) and A12: (a 'imp' b).x1=TRUE; A13: ('not' a.x1) 'or' b.x1=TRUE by A12,BVFUNC_1:def 8; A14: ('not' a.x1)=TRUE or ('not' a.x1)=FALSE by XBOOLEAN:def 3; per cases by A13,A14,BINARITH:3; suppose ('not' a.x1)=TRUE; then a.x1=FALSE by MARGREL1:11; then B_INF(a,CompF(PA,G)).z = FALSE by A11,BVFUNC_1:def 16; hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' FALSE) 'or' Ex(b,PA,G).z by A1,BVFUNC_1:def 8 .=TRUE 'or' Ex(b,PA,G).z by MARGREL1:11 .=TRUE by BINARITH:10; end; suppose b.x1=TRUE; then B_SUP(b,CompF(PA,G)).z = TRUE by A11,BVFUNC_1:def 17; then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10; hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; end; hence thesis by A2,BVFUNC_1:15; end; theorem All(a,PA,G) 'imp' All(b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G) proof let z be Element of Y; A1: ('not' All(a,PA,G).z)=TRUE or ('not' All(a,PA,G).z)=FALSE by XBOOLEAN:def 3 ; A2: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6; assume (All(a,PA,G) 'imp' All(b,PA,G)).z=TRUE; then A3: ('not' All(a,PA,G).z) 'or' All(b,PA,G).z=TRUE by BVFUNC_1:def 8; per cases by A3,A1,BINARITH:3; suppose 'not' All(a,PA,G).z=TRUE; hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =TRUE 'or' Ex(b,PA,G).z by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose A4: All(b,PA,G).z=TRUE; now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x=TRUE); then B_INF(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; hence contradiction by A4,BVFUNC_2:def 9; end; then b.z=TRUE by A2; then B_SUP(b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17; then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10; hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; end; theorem Ex(a,PA,G) 'imp' Ex(b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G) proof A1: Ex(a,PA,G) = B_SUP(a,CompF(PA,G)) by BVFUNC_2:def 10; let z be Element of Y; A2: ('not' Ex(a,PA,G).z)=TRUE or ('not' Ex(a,PA,G).z)=FALSE by XBOOLEAN:def 3; assume (Ex(a,PA,G) 'imp' Ex(b,PA,G)).z=TRUE; then A3: ('not' Ex(a,PA,G).z) 'or' Ex(b,PA,G).z=TRUE by BVFUNC_1:def 8; A4: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6; per cases by A3,A2,BINARITH:3; suppose ('not' Ex(a,PA,G).z)=TRUE; then Ex(a,PA,G).z=FALSE by MARGREL1:11; then a.z<>TRUE by A1,A4,BVFUNC_1:def 17; then B_INF(a,CompF(PA,G)).z = FALSE by A4,BVFUNC_1:def 16; then All(a,PA,G).z=FALSE by BVFUNC_2:def 9; hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' FALSE) 'or' Ex(b,PA,G).z by BVFUNC_1:def 8 .=TRUE 'or' Ex(b,PA,G).z by MARGREL1:11 .=TRUE by BINARITH:10; end; suppose Ex(b,PA,G).z=TRUE; hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; end; theorem Th26: All(a 'imp' b,PA,G) = All('not' a 'or' b,PA,G) proof A1: All('not' a 'or' b,PA,G) '<' All(a 'imp' b,PA,G) proof let z be Element of Y; assume A2: All('not' a 'or' b,PA,G).z=TRUE; A3: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds ('not' a 'or' b).x=TRUE); then B_INF('not' a 'or' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; hence contradiction by A2,BVFUNC_2:def 9; end; for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp' b).x=TRUE proof let x be Element of Y; A4: ('not' a).x=TRUE or ('not' a).x=FALSE by XBOOLEAN:def 3; assume x in EqClass(z,CompF(PA,G)); then ('not' a 'or' b).x=TRUE by A3; then A5: ('not' a).x 'or' b.x=TRUE by BVFUNC_1:def 4; per cases by A5,A4,BINARITH:3; suppose ('not' a).x=TRUE; then 'not' a.x=TRUE by MARGREL1:def 19; hence (a 'imp' b).x = TRUE 'or' b.x by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose b.x=TRUE; hence (a 'imp' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; end; then B_INF(a 'imp' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16; hence thesis by BVFUNC_2:def 9; end; All(a 'imp' b,PA,G) '<' All('not' a 'or' b,PA,G) proof let z be Element of Y; assume A6: All(a 'imp' b,PA,G).z=TRUE; A7: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp' b).x=TRUE); then B_INF(a 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; hence contradiction by A6,BVFUNC_2:def 9; end; now let x be Element of Y; A8: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3; assume x in EqClass(z,CompF(PA,G)); then (a 'imp' b).x=TRUE by A7; then A9: ('not' a.x) 'or' b.x=TRUE by BVFUNC_1:def 8; per cases by A9,A8,BINARITH:3; suppose ('not' a.x)=TRUE; then ('not' a).x=TRUE by MARGREL1:def 19; hence ('not' a 'or' b).x =TRUE 'or' b.x by BVFUNC_1:def 4 .=TRUE by BINARITH:10; end; suppose b.x=TRUE; hence ('not' a 'or' b).x=('not' a).x 'or' TRUE by BVFUNC_1:def 4 .=TRUE by BINARITH:10; end; end; then B_INF('not' a 'or' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16; hence thesis by BVFUNC_2:def 9; end; hence thesis by A1,BVFUNC_1:15; end; theorem All(a 'imp' b,PA,G) = 'not' (Ex(a '&' 'not' b,PA,G)) proof 'not' All('not' a 'or' b,PA,G) = Ex('not' ('not' a 'or' b),PA,G) & 'not' ( 'not' a 'or' b)=('not' 'not' a) '&' ('not' b) by BVFUNC_1:13,BVFUNC_2:18; hence thesis by Th26; end; theorem Ex(a,PA,G) '<' 'not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G )) proof let z be Element of Y; A1: ('not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G))).z ='not' (( All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G))).z by MARGREL1:def 19 .='not' (All(a 'imp' b,PA,G).z '&' (All(a 'imp' 'not' b,PA,G)).z) by MARGREL1:def 20; assume A2: Ex(a,PA,G).z=TRUE; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x= TRUE); then B_SUP(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; hence contradiction by A2,BVFUNC_2:def 10; end; then consider x1 being Element of Y such that A3: x1 in EqClass(z,CompF(PA,G)) and A4: a.x1=TRUE; A5: (a 'imp' b).x1 ='not' TRUE 'or' b.x1 by A4,BVFUNC_1:def 8 .=FALSE 'or' b.x1 by MARGREL1:11 .=b.x1 by BINARITH:3; A6: (a 'imp' 'not' b).x1 ='not' TRUE 'or' ('not' b).x1 by A4,BVFUNC_1:def 8 .=FALSE 'or' ('not' b).x1 by MARGREL1:11 .=('not' b).x1 by BINARITH:3; per cases by XBOOLEAN:def 3; suppose b.x1=TRUE; then (a 'imp' 'not' b).x1 ='not' TRUE by A6,MARGREL1:def 19 .=FALSE by MARGREL1:11; then (B_INF(a 'imp' 'not' b,CompF(PA,G))).z = FALSE by A3,BVFUNC_1:def 16; hence ('not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G))).z ='not' (All(a 'imp' b,PA,G).z '&' FALSE) by A1,BVFUNC_2:def 9 .='not' (FALSE) by MARGREL1:12 .=TRUE by MARGREL1:11; end; suppose b.x1=FALSE; then B_INF(a 'imp' b,CompF(PA,G)).z = FALSE by A3,A5,BVFUNC_1:def 16; hence ('not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G))).z ='not' (FALSE '&' (All(a 'imp' 'not' b,PA,G)).z) by A1,BVFUNC_2:def 9 .='not' (FALSE) by MARGREL1:12 .=TRUE by MARGREL1:11; end; end; theorem Ex(a,PA,G) '<' 'not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G)) proof let z be Element of Y; A1: ('not' Ex(a '&' 'not' b,PA,G)).z='not' (Ex(a '&' 'not' b,PA,G)).z by MARGREL1:def 19; A2: ('not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G))).z = 'not' (('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G))).z by MARGREL1:def 19 .='not' (('not' Ex(a '&' b,PA,G)).z '&' ('not' Ex(a '&' 'not' b,PA,G)).z ) by MARGREL1:def 20 .='not' ('not' Ex(a '&' b,PA,G).z '&' 'not' (Ex(a '&' 'not' b,PA,G)).z) by A1,MARGREL1:def 19; assume A3: Ex(a,PA,G).z=TRUE; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x= TRUE); then B_SUP(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; hence contradiction by A3,BVFUNC_2:def 10; end; then consider x1 being Element of Y such that A4: x1 in EqClass(z,CompF(PA,G)) and A5: a.x1=TRUE; A6: (a '&' b).x1 =TRUE '&' b.x1 by A5,MARGREL1:def 20 .=b.x1 by MARGREL1:14; A7: (a '&' 'not' b).x1 =TRUE '&' ('not' b).x1 by A5,MARGREL1:def 20 .=('not' b).x1 by MARGREL1:14; per cases by XBOOLEAN:def 3; suppose b.x1=TRUE; then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A4,A6,BVFUNC_1:def 17; hence ('not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G))).z = 'not' ('not' TRUE '&' 'not' (Ex(a '&' 'not' b,PA,G)).z) by A2, BVFUNC_2:def 10 .='not' (FALSE '&' 'not' (Ex(a '&' 'not' b,PA,G)).z) by MARGREL1:11 .='not' (FALSE) by MARGREL1:12 .=TRUE by MARGREL1:11; end; suppose b.x1=FALSE; then (a '&' 'not' b).x1='not' FALSE by A7,MARGREL1:def 19; then (a '&' 'not' b).x1=TRUE by MARGREL1:11; then (B_SUP(a '&' 'not' b,CompF(PA,G))).z = TRUE by A4,BVFUNC_1:def 17; hence ('not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G))).z = 'not' ('not' Ex(a '&' b,PA,G).z '&' 'not' TRUE) by A2,BVFUNC_2:def 10 .='not' ('not' Ex(a '&' b,PA,G).z '&' FALSE) by MARGREL1:11 .='not' (FALSE) by MARGREL1:12 .=TRUE by MARGREL1:11; end; end; theorem Ex(a,PA,G) '&' All(a 'imp' b,PA,G) '<' Ex(a '&' b,PA,G) proof let z be Element of Y; A1: 'not' FALSE=TRUE by MARGREL1:11; assume (Ex(a,PA,G) '&' All(a 'imp' b,PA,G)).z=TRUE; then A2: Ex(a,PA,G).z '&' All(a 'imp' b,PA,G).z=TRUE by MARGREL1:def 20; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x= TRUE); then B_SUP(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; then Ex(a,PA,G).z=FALSE by BVFUNC_2:def 10; hence contradiction by A2,MARGREL1:12; end; then consider x1 being Element of Y such that A3: x1 in EqClass(z,CompF(PA,G)) and A4: a.x1=TRUE; now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp' b).x=TRUE); then B_INF(a 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(a 'imp' b,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A2,MARGREL1:12; end; then (a 'imp' b).x1=TRUE by A3; then A5: ('not' a.x1) 'or' b.x1 =TRUE by BVFUNC_1:def 8; (a '&' b).x1 =a.x1 '&' b.x1 by MARGREL1:def 20 .=TRUE '&' TRUE by A4,A5,A1,BINARITH:3 .=TRUE; then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A3,BVFUNC_1:def 17; hence thesis by BVFUNC_2:def 10; end; theorem Ex(a,PA,G) '&' 'not' Ex(a '&' b,PA,G) '<' 'not' All(a 'imp' b,PA,G) proof let z be Element of Y; assume (Ex(a,PA,G) '&' 'not' Ex(a '&' b,PA,G)).z=TRUE; then A1: Ex(a,PA,G).z '&' ('not' Ex(a '&' b,PA,G)).z=TRUE by MARGREL1:def 20; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x= TRUE); then B_SUP(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; then Ex(a,PA,G).z=FALSE by BVFUNC_2:def 10; hence contradiction by A1,MARGREL1:12; end; then consider x1 being Element of Y such that A2: x1 in EqClass(z,CompF(PA,G)) and A3: a.x1=TRUE; ('not' Ex(a '&' b,PA,G)).z=TRUE by A1,MARGREL1:12; then 'not' Ex(a '&' b,PA,G).z=TRUE by MARGREL1:def 19; then Ex(a '&' b,PA,G) = B_SUP(a '&' b,CompF(PA,G)) & Ex(a '&' b,PA,G).z=FALSE by BVFUNC_2:def 10,MARGREL1:11; then (a '&' b).x1<>TRUE by A2,BVFUNC_1:def 17; then (a '&' b).x1=FALSE by XBOOLEAN:def 3; then A4: a.x1 '&' b.x1=FALSE by MARGREL1:def 20; per cases by A4,MARGREL1:12; suppose a.x1=FALSE; hence thesis by A3; end; suppose b.x1=FALSE; then (a 'imp' b).x1 =('not' TRUE) 'or' FALSE by A3,BVFUNC_1:def 8 .=FALSE 'or' FALSE by MARGREL1:11 .=FALSE; then B_INF(a 'imp' b,CompF(PA,G)).z = FALSE by A2,BVFUNC_1:def 16; then All(a 'imp' b,PA,G).z=FALSE by BVFUNC_2:def 9; hence ('not' All(a 'imp' b,PA,G)).z ='not' FALSE by MARGREL1:def 19 .=TRUE by MARGREL1:11; end; end; theorem All(a 'imp' c,PA,G) '&' All(c 'imp' b,PA,G) '<' All(a 'imp' b,PA,G) proof let z be Element of Y; assume (All(a 'imp' c,PA,G) '&' All(c 'imp' b,PA,G)).z=TRUE; then A1: All(a 'imp' c,PA,G).z '&' All(c 'imp' b,PA,G).z=TRUE by MARGREL1:def 20; A2: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (c 'imp' b).x=TRUE); then B_INF(c 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(c 'imp' b,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; A3: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp' c).x=TRUE); then B_INF(a 'imp' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(a 'imp' c,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp' b).x=TRUE proof let x be Element of Y; A4: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3; A5: ('not' c.x)=TRUE or ('not' c.x)=FALSE by XBOOLEAN:def 3; assume A6: x in EqClass(z,CompF(PA,G)); then (a 'imp' c).x=TRUE by A3; then A7: ('not' a.x) 'or' c.x=TRUE by BVFUNC_1:def 8; (c 'imp' b).x=TRUE by A2,A6; then A8: ('not' c.x) 'or' b.x=TRUE by BVFUNC_1:def 8; per cases by A7,A4,A8,A5,BINARITH:3; suppose ('not' a.x)=TRUE & ('not' c.x)=TRUE; hence (a 'imp' b).x =TRUE 'or' b.x by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose ('not' a.x)=TRUE & b.x=TRUE; hence (a 'imp' b).x =TRUE 'or' b.x by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose c.x=TRUE & ('not' c.x)=TRUE; hence thesis by MARGREL1:11; end; suppose c.x=TRUE & b.x=TRUE; hence (a 'imp' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; end; then B_INF(a 'imp' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16; hence thesis by BVFUNC_2:def 9; end; theorem All(c 'imp' b,PA,G) '&' Ex(a '&' c,PA,G) '<' Ex(a '&' b,PA,G) proof let z be Element of Y; assume (All(c 'imp' b,PA,G) '&' Ex(a '&' c,PA,G)).z=TRUE; then A1: All(c 'imp' b,PA,G).z '&' Ex(a '&' c,PA,G).z=TRUE by MARGREL1:def 20; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & (a '&' c).x=TRUE); then B_SUP(a '&' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; then Ex(a '&' c,PA,G).z=FALSE by BVFUNC_2:def 10; hence contradiction by A1,MARGREL1:12; end; then consider x1 being Element of Y such that A2: x1 in EqClass(z,CompF(PA,G)) and A3: (a '&' c).x1=TRUE; A4: a.x1 '&' c.x1=TRUE by A3,MARGREL1:def 20; now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (c 'imp' b).x=TRUE); then B_INF(c 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(c 'imp' b,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; then (c 'imp' b).x1=TRUE by A2; then A5: ('not' c.x1) 'or' b.x1=TRUE by BVFUNC_1:def 8; A6: ('not' c.x1)=TRUE or ('not' c.x1)=FALSE by XBOOLEAN:def 3; per cases by A5,A6,A4,BINARITH:3,MARGREL1:12; suppose a.x1=TRUE & c.x1=TRUE & ('not' c.x1)=TRUE; hence thesis by MARGREL1:11; end; suppose a.x1=TRUE & c.x1=TRUE & b.x1=TRUE; then (a '&' b).x1 =TRUE '&' TRUE by MARGREL1:def 20 .=TRUE; then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17; hence thesis by BVFUNC_2:def 10; end; end; theorem All(b 'imp' 'not' c,PA,G) '&' All(a 'imp' c,PA,G) '<' All(a 'imp' 'not' b,PA,G) proof let z be Element of Y; assume (All(b 'imp' 'not' c,PA,G) '&' All(a 'imp' c,PA,G)).z=TRUE; then A1: All(b 'imp' 'not' c,PA,G).z '&' All(a 'imp' c,PA,G).z=TRUE by MARGREL1:def 20; A2: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp' c).x=TRUE); then B_INF(a 'imp' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(a 'imp' c,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; A3: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (b 'imp' 'not' c).x=TRUE); then B_INF(b 'imp' 'not' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(b 'imp' 'not' c,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp' 'not' b).x=TRUE proof let x be Element of Y; A4: ('not' b.x)=TRUE or ('not' b.x)=FALSE by XBOOLEAN:def 3; A5: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3; assume A6: x in EqClass(z,CompF(PA,G)); then (b 'imp' 'not' c).x=TRUE by A3; then A7: ('not' b.x) 'or' ('not' c).x=TRUE by BVFUNC_1:def 8; (a 'imp' c).x=TRUE by A2,A6; then A8: ('not' a.x) 'or' c.x=TRUE by BVFUNC_1:def 8; per cases by A7,A4,A8,A5,BINARITH:3; suppose A9: ('not' b.x)=TRUE & ('not' a.x)=TRUE; then ('not' b).x=TRUE by MARGREL1:def 19; hence (a 'imp' 'not' b).x =TRUE 'or' TRUE by A9,BVFUNC_1:def 8 .=TRUE; end; suppose ('not' b.x)=TRUE & c.x=TRUE; then ('not' b).x=TRUE by MARGREL1:def 19; hence (a 'imp' 'not' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose ('not' c).x=TRUE & ('not' a.x)=TRUE; hence (a 'imp' 'not' b).x =TRUE 'or' ('not' b).x by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose A10: ('not' c).x=TRUE & c.x=TRUE; then 'not' c.x=TRUE by MARGREL1:def 19; hence thesis by A10,MARGREL1:11; end; end; then B_INF(a 'imp' 'not' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16; hence thesis by BVFUNC_2:def 9; end; theorem All(b 'imp' c,PA,G) '&' All(a 'imp' 'not' c,PA,G) '<' All(a 'imp' 'not' b,PA,G) proof let z be Element of Y; assume (All(b 'imp' c,PA,G) '&' All(a 'imp' 'not' c,PA,G)).z=TRUE; then A1: All(b 'imp' c,PA,G).z '&' All(a 'imp' 'not' c,PA,G).z=TRUE by MARGREL1:def 20; A2: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp' 'not' c).x=TRUE); then B_INF(a 'imp' 'not' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(a 'imp' 'not' c,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; A3: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (b 'imp' c).x=TRUE); then B_INF(b 'imp' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(b 'imp' c,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp' 'not' b).x=TRUE proof let x be Element of Y; A4: ('not' b.x)=TRUE or ('not' b.x)=FALSE by XBOOLEAN:def 3; A5: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3; assume A6: x in EqClass(z,CompF(PA,G)); then (b 'imp' c).x=TRUE by A3; then A7: ('not' b.x) 'or' c.x=TRUE by BVFUNC_1:def 8; (a 'imp' 'not' c).x=TRUE by A2,A6; then A8: ('not' a.x) 'or' ('not' c).x=TRUE by BVFUNC_1:def 8; per cases by A7,A4,A8,A5,BINARITH:3; suppose A9: ('not' b.x)=TRUE & ('not' a.x)=TRUE; then ('not' b).x=TRUE by MARGREL1:def 19; hence (a 'imp' 'not' b).x =TRUE 'or' TRUE by A9,BVFUNC_1:def 8 .=TRUE; end; suppose ('not' b.x)=TRUE & ('not' c).x=TRUE; then ('not' b).x=TRUE by MARGREL1:def 19; hence (a 'imp' 'not' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose c.x=TRUE & ('not' a.x)=TRUE; hence (a 'imp' 'not' b).x =TRUE 'or' ('not' b).x by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose A10: c.x=TRUE & ('not' c).x=TRUE; then 'not' c.x=TRUE by MARGREL1:def 19; hence thesis by A10,MARGREL1:11; end; end; then B_INF(a 'imp' 'not' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16; hence thesis by BVFUNC_2:def 9; end; theorem All(b 'imp' 'not' c,PA,G) '&' Ex(a '&' c,PA,G) '<' Ex(a '&' 'not' b,PA ,G ) proof let z be Element of Y; assume (All(b 'imp' 'not' c,PA,G) '&' Ex(a '&' c,PA,G)).z=TRUE; then A1: All(b 'imp' 'not' c,PA,G).z '&' Ex(a '&' c,PA,G).z=TRUE by MARGREL1:def 20; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & (a '&' c).x=TRUE); then B_SUP(a '&' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; then Ex(a '&' c,PA,G).z=FALSE by BVFUNC_2:def 10; hence contradiction by A1,MARGREL1:12; end; then consider x1 being Element of Y such that A2: x1 in EqClass(z,CompF(PA,G)) and A3: (a '&' c).x1=TRUE; A4: a.x1 '&' c.x1=TRUE by A3,MARGREL1:def 20; now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (b 'imp' 'not' c).x=TRUE); then B_INF(b 'imp' 'not' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(b 'imp' 'not' c,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; then (b 'imp' 'not' c).x1=TRUE by A2; then A5: ('not' b.x1) 'or' ('not' c).x1=TRUE by BVFUNC_1:def 8; A6: ('not' b.x1)=TRUE or ('not' b.x1)=FALSE by XBOOLEAN:def 3; per cases by A5,A6,A4,BINARITH:3,MARGREL1:12; suppose A7: a.x1=TRUE & c.x1=TRUE & ('not' b.x1)=TRUE; (a '&' 'not' b).x1 =a.x1 '&' ('not' b).x1 by MARGREL1:def 20 .=TRUE '&' TRUE by A7,MARGREL1:def 19 .=TRUE; then B_SUP(a '&' 'not' b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17; hence thesis by BVFUNC_2:def 10; end; suppose A8: a.x1=TRUE & c.x1=TRUE & ('not' c).x1=TRUE; then 'not' c.x1=TRUE by MARGREL1:def 19; hence thesis by A8,MARGREL1:11; end; end; theorem All(b 'imp' c,PA,G) '&' Ex(a '&' 'not' c,PA,G) '<' Ex(a '&' 'not' b,PA ,G ) proof let z be Element of Y; assume (All(b 'imp' c,PA,G) '&' Ex(a '&' 'not' c,PA,G)).z=TRUE; then A1: All(b 'imp' c,PA,G).z '&' Ex(a '&' 'not' c,PA,G).z=TRUE by MARGREL1:def 20; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & (a '&' 'not' c).x=TRUE); then B_SUP(a '&' 'not' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; then Ex(a '&' 'not' c,PA,G).z=FALSE by BVFUNC_2:def 10; hence contradiction by A1,MARGREL1:12; end; then consider x1 being Element of Y such that A2: x1 in EqClass(z,CompF(PA,G)) and A3: (a '&' 'not' c).x1=TRUE; A4: a.x1 '&' ('not' c).x1=TRUE by A3,MARGREL1:def 20; now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (b 'imp' c).x=TRUE); then B_INF(b 'imp' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(b 'imp' c,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; then (b 'imp' c).x1=TRUE by A2; then A5: ('not' b.x1) 'or' c.x1=TRUE by BVFUNC_1:def 8; A6: ('not' b.x1)=TRUE or ('not' b.x1)=FALSE by XBOOLEAN:def 3; per cases by A5,A6,A4,BINARITH:3,MARGREL1:12; suppose A7: a.x1=TRUE & ('not' c).x1=TRUE & ('not' b.x1)=TRUE; (a '&' 'not' b).x1 = a.x1 '&' ('not' b).x1 by MARGREL1:def 20 .=TRUE '&' TRUE by A7,MARGREL1:def 19 .=TRUE; then B_SUP(a '&' 'not' b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17; hence thesis by BVFUNC_2:def 10; end; suppose A8: a.x1=TRUE & ('not' c).x1=TRUE & c.x1=TRUE; then 'not' c.x1=TRUE by MARGREL1:def 19; hence thesis by A8,MARGREL1:11; end; end; theorem Ex(c,PA,G) '&' All(c 'imp' b,PA,G) '&' All(c 'imp' a,PA,G) '<' Ex(a '&' b,PA,G) proof let z be Element of Y; assume (Ex(c,PA,G) '&' All(c 'imp' b,PA,G) '&' All(c 'imp' a,PA,G)).z=TRUE; then A1: (Ex(c,PA,G) '&' All(c 'imp' b,PA,G)).z '&' All(c 'imp' a,PA,G).z = TRUE by MARGREL1:def 20; then Ex(c,PA,G).z '&' All(c 'imp' b,PA,G).z '&' All(c 'imp' a,PA,G).z=TRUE by MARGREL1:def 20; then A2: Ex(c,PA,G).z '&' All(c 'imp' b,PA,G).z=TRUE by MARGREL1:12; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & c.x= TRUE); then B_SUP(c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; then Ex(c,PA,G).z=FALSE by BVFUNC_2:def 10; hence contradiction by A2,MARGREL1:12; end; then consider x1 being Element of Y such that A3: x1 in EqClass(z,CompF(PA,G)) and A4: c.x1=TRUE; A5: ('not' c.x1)=TRUE or ('not' c.x1)=FALSE by XBOOLEAN:def 3; now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (c 'imp' b).x=TRUE); then B_INF(c 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(c 'imp' b,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A2,MARGREL1:12; end; then (c 'imp' b).x1=TRUE by A3; then A6: ('not' c.x1) 'or' b.x1=TRUE by BVFUNC_1:def 8; now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (c 'imp' a).x=TRUE); then B_INF(c 'imp' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(c 'imp' a,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; then (c 'imp' a).x1=TRUE by A3; then A7: ('not' c.x1) 'or' a.x1=TRUE by BVFUNC_1:def 8; per cases by A7,A5,A6,BINARITH:3; suppose ('not' c.x1)=TRUE; hence thesis by A4,MARGREL1:11; end; suppose ('not' c.x1)=TRUE & b.x1=TRUE; hence thesis by A4,MARGREL1:11; end; suppose a.x1=TRUE & ('not' c.x1)=TRUE; hence thesis by A4,MARGREL1:11; end; suppose a.x1=TRUE & b.x1=TRUE; then (a '&' b).x1 =TRUE '&' TRUE by MARGREL1:def 20 .=TRUE; then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A3,BVFUNC_1:def 17; hence thesis by BVFUNC_2:def 10; end; end; theorem All(b 'imp' c,PA,G) '&' All(c 'imp' 'not' a,PA,G) '<' All(a 'imp' 'not' b,PA,G) proof let z be Element of Y; assume (All(b 'imp' c,PA,G) '&' All(c 'imp' 'not' a,PA,G)).z=TRUE; then A1: All(b 'imp' c,PA,G).z '&' All(c 'imp' 'not' a,PA,G).z=TRUE by MARGREL1:def 20; A2: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (b 'imp' c).x=TRUE); then B_INF(b 'imp' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(b 'imp' c,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; A3: now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (c 'imp' 'not' a).x=TRUE); then B_INF(c 'imp' 'not' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(c 'imp' 'not' a,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp' 'not' b).x=TRUE proof let x be Element of Y; A4: ('not' c.x)=TRUE or ('not' c.x)=FALSE by XBOOLEAN:def 3; A5: ('not' b.x)=TRUE or ('not' b.x)=FALSE by XBOOLEAN:def 3; assume A6: x in EqClass(z,CompF(PA,G)); then (c 'imp' 'not' a).x=TRUE by A3; then A7: ('not' c.x) 'or' ('not' a).x=TRUE by BVFUNC_1:def 8; (b 'imp' c).x=TRUE by A2,A6; then A8: ('not' b.x) 'or' c.x=TRUE by BVFUNC_1:def 8; per cases by A7,A4,A8,A5,BINARITH:3; suppose ('not' c.x)=TRUE & ('not' b.x)=TRUE; then ('not' b).x=TRUE by MARGREL1:def 19; hence (a 'imp' 'not' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose ('not' c.x)=TRUE & c.x=TRUE; hence thesis by MARGREL1:11; end; suppose ('not' a).x=TRUE & ('not' b.x)=TRUE; then ('not' b).x=TRUE by MARGREL1:def 19; hence (a 'imp' 'not' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; suppose ('not' a).x=TRUE & c.x=TRUE; then 'not' a.x=TRUE by MARGREL1:def 19; hence (a 'imp' 'not' b).x =TRUE 'or' ('not' b).x by BVFUNC_1:def 8 .=TRUE by BINARITH:10; end; end; then B_INF(a 'imp' 'not' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16; hence thesis by BVFUNC_2:def 9; end; theorem Ex(b,PA,G) '&' All(b 'imp' c,PA,G) '&' All(c 'imp' a,PA,G) '<' Ex(a '&' b,PA,G) proof let z be Element of Y; assume (Ex(b,PA,G) '&' All(b 'imp' c,PA,G) '&' All(c 'imp' a,PA,G)).z=TRUE; then A1: (Ex(b,PA,G) '&' All(b 'imp' c,PA,G)).z '&' All(c 'imp' a,PA,G).z= TRUE by MARGREL1:def 20; then Ex(b,PA,G).z '&' All(b 'imp' c,PA,G).z '&' All(c 'imp' a,PA,G).z=TRUE by MARGREL1:def 20; then A2: (Ex(b,PA,G).z '&' All(b 'imp' c,PA,G).z)=TRUE by MARGREL1:12; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x= TRUE); then B_SUP(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; then Ex(b,PA,G).z=FALSE by BVFUNC_2:def 10; hence contradiction by A2,MARGREL1:12; end; then consider x1 being Element of Y such that A3: x1 in EqClass(z,CompF(PA,G)) and A4: b.x1=TRUE; A5: ('not' c.x1)=TRUE or ('not' c.x1)=FALSE by XBOOLEAN:def 3; now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (c 'imp' a).x=TRUE); then B_INF(c 'imp' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(c 'imp' a,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; then (c 'imp' a).x1=TRUE by A3; then A6: ('not' c.x1) 'or' a.x1=TRUE by BVFUNC_1:def 8; A7: ('not' b.x1)=TRUE or ('not' b.x1)=FALSE by XBOOLEAN:def 3; now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (b 'imp' c).x=TRUE); then B_INF(b 'imp' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(b 'imp' c,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A2,MARGREL1:12; end; then (b 'imp' c).x1=TRUE by A3; then A8: ('not' b.x1) 'or' c.x1=TRUE by BVFUNC_1:def 8; per cases by A6,A5,A8,A7,BINARITH:3; suppose ('not' c.x1)=TRUE & ('not' b.x1)=TRUE; hence thesis by A4,MARGREL1:11; end; suppose ('not' c.x1)=TRUE & c.x1=TRUE; hence thesis by MARGREL1:11; end; suppose a.x1=TRUE & ('not' b.x1)=TRUE; hence thesis by A4,MARGREL1:11; end; suppose a.x1=TRUE & c.x1=TRUE; then (a '&' b).x1 =TRUE '&' TRUE by A4,MARGREL1:def 20 .=TRUE; then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A3,BVFUNC_1:def 17; hence thesis by BVFUNC_2:def 10; end; end; theorem Ex(c,PA,G) '&' All(b 'imp' 'not' c,PA,G) '&' All(c 'imp' a,PA,G) '<' Ex(a '&' 'not' b,PA,G) proof let z be Element of Y; assume (Ex(c,PA,G) '&' All(b 'imp' 'not' c,PA,G) '&' All(c 'imp' a,PA,G)).z =TRUE; then A1: (Ex(c,PA,G) '&' All(b 'imp' 'not' c,PA,G)).z '&' All(c 'imp' a,PA,G).z= TRUE by MARGREL1:def 20; then Ex(c,PA,G).z '&' All(b 'imp' 'not' c,PA,G).z '&' All(c 'imp' a,PA,G).z= TRUE by MARGREL1:def 20; then A2: Ex(c,PA,G).z '&' All(b 'imp' 'not' c,PA,G).z=TRUE by MARGREL1:12; now assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & c.x= TRUE); then B_SUP(c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17; then Ex(c,PA,G).z=FALSE by BVFUNC_2:def 10; hence contradiction by A2,MARGREL1:12; end; then consider x1 being Element of Y such that A3: x1 in EqClass(z,CompF(PA,G)) and A4: c.x1=TRUE; A5: ('not' c.x1)=TRUE or ('not' c.x1)=FALSE by XBOOLEAN:def 3; now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (c 'imp' a).x=TRUE); then B_INF(c 'imp' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(c 'imp' a,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A1,MARGREL1:12; end; then (c 'imp' a).x1=TRUE by A3; then A6: ('not' c.x1) 'or' a.x1=TRUE by BVFUNC_1:def 8; A7: ('not' b.x1)=TRUE or ('not' b.x1)=FALSE by XBOOLEAN:def 3; now assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (b 'imp' 'not' c).x=TRUE); then B_INF(b 'imp' 'not' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16; then All(b 'imp' 'not' c,PA,G).z=FALSE by BVFUNC_2:def 9; hence contradiction by A2,MARGREL1:12; end; then (b 'imp' 'not' c).x1=TRUE by A3; then A8: ('not' b.x1) 'or' ('not' c).x1=TRUE by BVFUNC_1:def 8; per cases by A6,A5,A8,A7,BINARITH:3; suppose ('not' c.x1)=TRUE & ('not' b.x1)=TRUE; hence thesis by A4,MARGREL1:11; end; suppose ('not' c.x1)=TRUE & ('not' c).x1=TRUE; hence thesis by A4,MARGREL1:11; end; suppose A9: a.x1=TRUE & ('not' b.x1)=TRUE; (a '&' 'not' b).x1 =a.x1 '&' ('not' b).x1 by MARGREL1:def 20 .=TRUE '&' TRUE by A9,MARGREL1:def 19 .=TRUE; then B_SUP(a '&' 'not' b,CompF(PA,G)).z=TRUE by A3,BVFUNC_1:def 17; hence thesis by BVFUNC_2:def 10; end; suppose a.x1=TRUE & ('not' c).x1=TRUE; then 'not' c.x1=TRUE by MARGREL1:def 19; hence thesis by A4,MARGREL1:11; end; end;