:: BVFUNC_4 semantic presentation begin theorem :: BVFUNC_4:1 for Y being non empty set for a, b, c being Function of Y,BOOLEAN st a '<' b 'imp' c holds a '&' b '<' c proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st a '<' b 'imp' c holds a '&' b '<' c let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a '<' b 'imp' c implies a '&' b '<' c ) assume A1: a '<' b 'imp' c ; ::_thesis: a '&' b '<' c for x being Element of Y holds ((a '&' b) 'imp' c) . x = TRUE proof let x be Element of Y; ::_thesis: ((a '&' b) 'imp' c) . x = TRUE A2: (a 'imp' (b 'imp' c)) . x = ('not' (a . x)) 'or' ((b 'imp' c) . x) by BVFUNC_1:def_8 .= ('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)) by BVFUNC_1:def_8 .= (('not' (a . x)) 'or' ('not' (b . x))) 'or' (c . x) ; A3: ((a '&' b) 'imp' c) . x = ('not' ((a '&' b) . x)) 'or' (c . x) by BVFUNC_1:def_8 .= (('not' (a . x)) 'or' ('not' (b . x))) 'or' (c . x) by MARGREL1:def_20 ; a 'imp' (b 'imp' c) = I_el Y by A1, BVFUNC_1:16; hence ((a '&' b) 'imp' c) . x = TRUE by A2, A3, BVFUNC_1:def_11; ::_thesis: verum end; then (a '&' b) 'imp' c = I_el Y by BVFUNC_1:def_11; hence a '&' b '<' c by BVFUNC_1:16; ::_thesis: verum end; theorem :: BVFUNC_4:2 for Y being non empty set for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds a '<' b 'imp' c proof let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds a '<' b 'imp' c let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a '&' b '<' c implies a '<' b 'imp' c ) assume A1: a '&' b '<' c ; ::_thesis: a '<' b 'imp' c for x being Element of Y holds (a 'imp' (b 'imp' c)) . x = TRUE proof let x be Element of Y; ::_thesis: (a 'imp' (b 'imp' c)) . x = TRUE A2: (a 'imp' (b 'imp' c)) . x = ('not' (a . x)) 'or' ((b 'imp' c) . x) by BVFUNC_1:def_8 .= ('not' (a . x)) 'or' (('not' (b . x)) 'or' (c . x)) by BVFUNC_1:def_8 .= (('not' (a . x)) 'or' ('not' (b . x))) 'or' (c . x) ; A3: ((a '&' b) 'imp' c) . x = ('not' ((a '&' b) . x)) 'or' (c . x) by BVFUNC_1:def_8 .= (('not' (a . x)) 'or' ('not' (b . x))) 'or' (c . x) by MARGREL1:def_20 ; (a '&' b) 'imp' c = I_el Y by A1, BVFUNC_1:16; hence (a 'imp' (b 'imp' c)) . x = TRUE by A2, A3, BVFUNC_1:def_11; ::_thesis: verum end; then a 'imp' (b 'imp' c) = I_el Y by BVFUNC_1:def_11; hence a '<' b 'imp' c by BVFUNC_1:16; ::_thesis: verum end; theorem :: BVFUNC_4:3 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'or' (a '&' b) = a proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'or' (a '&' b) = a let a, b be Function of Y,BOOLEAN; ::_thesis: a 'or' (a '&' b) = a let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'or' (a '&' b)) . x = a . x thus (a 'or' (a '&' b)) . x = (a . x) 'or' ((a '&' b) . x) by BVFUNC_1:def_4 .= (a . x) 'or' ((a . x) '&' (b . x)) by MARGREL1:def_20 .= a . x by XBOOLEAN:5 ; ::_thesis: verum end; theorem :: BVFUNC_4:4 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a '&' (a 'or' b) = a proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '&' (a 'or' b) = a let a, b be Function of Y,BOOLEAN; ::_thesis: a '&' (a 'or' b) = a let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a '&' (a 'or' b)) . x = a . x thus (a '&' (a 'or' b)) . x = (a . x) '&' ((a 'or' b) . x) by MARGREL1:def_20 .= (a . x) '&' ((a . x) 'or' (b . x)) by BVFUNC_1:def_4 .= a . x by XBOOLEAN:6 ; ::_thesis: verum end; theorem Th5: :: BVFUNC_4:5 for Y being non empty set for a being Function of Y,BOOLEAN holds a '&' ('not' a) = O_el Y proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a '&' ('not' a) = O_el Y let a be Function of Y,BOOLEAN; ::_thesis: a '&' ('not' a) = O_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a '&' ('not' a)) . x = (O_el Y) . x thus (a '&' ('not' a)) . x = (a . x) '&' (('not' a) . x) by MARGREL1:def_20 .= (a . x) '&' ('not' (a . x)) by MARGREL1:def_19 .= FALSE by XBOOLEAN:138 .= (O_el Y) . x by BVFUNC_1:def_10 ; ::_thesis: verum end; theorem :: BVFUNC_4:6 for Y being non empty set for a being Function of Y,BOOLEAN holds a 'or' ('not' a) = I_el Y proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN holds a 'or' ('not' a) = I_el Y let a be Function of Y,BOOLEAN; ::_thesis: a 'or' ('not' a) = I_el Y let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'or' ('not' a)) . x = (I_el Y) . x thus (a 'or' ('not' a)) . x = (a . x) 'or' (('not' a) . x) by BVFUNC_1:def_4 .= (a . x) 'or' ('not' (a . x)) by MARGREL1:def_19 .= TRUE by XBOOLEAN:102 .= (I_el Y) . x by BVFUNC_1:def_11 ; ::_thesis: verum end; theorem Th7: :: BVFUNC_4:7 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'imp' b) '&' (b 'imp' a) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'imp' b) '&' (b 'imp' a) let a, b be Function of Y,BOOLEAN; ::_thesis: a 'eqv' b = (a 'imp' b) '&' (b 'imp' a) let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'eqv' b) . x = ((a 'imp' b) '&' (b 'imp' a)) . x thus (a 'eqv' b) . x = (a . x) <=> (b . x) by BVFUNC_1:def_9 .= ((a . x) => (b . x)) '&' ((b . x) => (a . x)) .= ((a 'imp' b) . x) '&' ((b . x) => (a . x)) by BVFUNC_1:def_8 .= ((a 'imp' b) . x) '&' ((b 'imp' a) . x) by BVFUNC_1:def_8 .= ((a 'imp' b) '&' (b 'imp' a)) . x by MARGREL1:def_20 ; ::_thesis: verum end; theorem Th8: :: BVFUNC_4:8 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' a) 'or' b proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' a) 'or' b let a, b be Function of Y,BOOLEAN; ::_thesis: a 'imp' b = ('not' a) 'or' b let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'imp' b) . x = (('not' a) 'or' b) . x thus (a 'imp' b) . x = (a . x) => (b . x) by BVFUNC_1:def_8 .= ('not' (a . x)) 'or' (b . x) .= (('not' a) . x) 'or' (b . x) by MARGREL1:def_19 .= (('not' a) 'or' b) . x by BVFUNC_1:def_4 ; ::_thesis: verum end; theorem :: BVFUNC_4:9 for Y being non empty set for a, b being Function of Y,BOOLEAN holds a 'xor' b = (('not' a) '&' b) 'or' (a '&' ('not' b)) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a 'xor' b = (('not' a) '&' b) 'or' (a '&' ('not' b)) let a, b be Function of Y,BOOLEAN; ::_thesis: a 'xor' b = (('not' a) '&' b) 'or' (a '&' ('not' b)) let x be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (a 'xor' b) . x = ((('not' a) '&' b) 'or' (a '&' ('not' b))) . x thus (a 'xor' b) . x = (a . x) 'xor' (b . x) by BVFUNC_1:def_5 .= (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) .= (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' (('not' b) . x)) by MARGREL1:def_19 .= ((('not' a) . x) '&' (b . x)) 'or' ((a . x) '&' (('not' b) . x)) by MARGREL1:def_19 .= ((('not' a) '&' b) . x) 'or' ((a . x) '&' (('not' b) . x)) by MARGREL1:def_20 .= ((('not' a) '&' b) . x) 'or' ((a '&' ('not' b)) . x) by MARGREL1:def_20 .= ((('not' a) '&' b) 'or' (a '&' ('not' b))) . x by BVFUNC_1:def_4 ; ::_thesis: verum end; theorem Th10: :: BVFUNC_4:10 for Y being non empty set for a, b being Function of Y,BOOLEAN holds ( a 'eqv' b = I_el Y iff ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) ) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds ( a 'eqv' b = I_el Y iff ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) ) let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y iff ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) ) thus ( a 'eqv' b = I_el Y implies ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) ) ::_thesis: ( a 'imp' b = I_el Y & b 'imp' a = I_el Y implies a 'eqv' b = I_el Y ) proof assume a 'eqv' b = I_el Y ; ::_thesis: ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) then a = b by BVFUNC_1:17; hence ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) by BVFUNC_1:16; ::_thesis: verum end; assume ( a 'imp' b = I_el Y & b 'imp' a = I_el Y ) ; ::_thesis: a 'eqv' b = I_el Y then a 'eqv' b = (I_el Y) '&' (I_el Y) by Th7; hence a 'eqv' b = I_el Y ; ::_thesis: verum end; theorem :: BVFUNC_4:11 for Y being non empty set for a, b being Function of Y,BOOLEAN st a 'eqv' b = I_el Y holds ('not' a) 'eqv' ('not' b) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN st a 'eqv' b = I_el Y holds ('not' a) 'eqv' ('not' b) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y implies ('not' a) 'eqv' ('not' b) = I_el Y ) assume a 'eqv' b = I_el Y ; ::_thesis: ('not' a) 'eqv' ('not' b) = I_el Y then a = b by BVFUNC_1:17; hence ('not' a) 'eqv' ('not' b) = I_el Y by BVFUNC_1:17; ::_thesis: verum end; theorem :: BVFUNC_4:12 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds (a '&' c) 'eqv' (b '&' d) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds (a '&' c) 'eqv' (b '&' d) = I_el Y let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y implies (a '&' c) 'eqv' (b '&' d) = I_el Y ) assume ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y ) ; ::_thesis: (a '&' c) 'eqv' (b '&' d) = I_el Y then ( a = b & c = d ) by BVFUNC_1:17; hence (a '&' c) 'eqv' (b '&' d) = I_el Y by BVFUNC_1:17; ::_thesis: verum end; theorem :: BVFUNC_4:13 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds (a 'imp' c) 'eqv' (b 'imp' d) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds (a 'imp' c) 'eqv' (b 'imp' d) = I_el Y let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y implies (a 'imp' c) 'eqv' (b 'imp' d) = I_el Y ) assume ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y ) ; ::_thesis: (a 'imp' c) 'eqv' (b 'imp' d) = I_el Y then ( a = b & c = d ) by BVFUNC_1:17; hence (a 'imp' c) 'eqv' (b 'imp' d) = I_el Y by BVFUNC_1:17; ::_thesis: verum end; theorem :: BVFUNC_4:14 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds (a 'or' c) 'eqv' (b 'or' d) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds (a 'or' c) 'eqv' (b 'or' d) = I_el Y let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y implies (a 'or' c) 'eqv' (b 'or' d) = I_el Y ) assume ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y ) ; ::_thesis: (a 'or' c) 'eqv' (b 'or' d) = I_el Y then ( a = b & c = d ) by BVFUNC_1:17; hence (a 'or' c) 'eqv' (b 'or' d) = I_el Y by BVFUNC_1:17; ::_thesis: verum end; theorem :: BVFUNC_4:15 for Y being non empty set for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds (a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN st a 'eqv' b = I_el Y & c 'eqv' d = I_el Y holds (a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y implies (a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y ) assume ( a 'eqv' b = I_el Y & c 'eqv' d = I_el Y ) ; ::_thesis: (a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y then ( a = b & c = d ) by BVFUNC_1:17; hence (a 'eqv' c) 'eqv' (b 'eqv' d) = I_el Y by BVFUNC_1:17; ::_thesis: verum end; begin theorem :: BVFUNC_4:16 for Y being non empty set for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G)) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G)) let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G)) let PA be a_partition of Y; ::_thesis: All ((a 'eqv' b),PA,G) = (All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G)) let z be Element of Y; :: according to FUNCT_2:def_8 ::_thesis: (All ((a 'eqv' b),PA,G)) . z = ((All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))) . z (All ((a 'eqv' b),PA,G)) . z = (All (((a 'imp' b) '&' (b 'imp' a)),PA,G)) . z by Th7 .= ((All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))) . z by BVFUNC_1:39 ; hence (All ((a 'eqv' b),PA,G)) . z = ((All ((a 'imp' b),PA,G)) '&' (All ((b 'imp' a),PA,G))) . z ; ::_thesis: verum end; theorem :: BVFUNC_4:17 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G) let G be Subset of (PARTITIONS Y); ::_thesis: for PA, PB being a_partition of Y holds All (a,PA,G) '<' Ex (a,PB,G) let PA, PB be a_partition of Y; ::_thesis: All (a,PA,G) '<' Ex (a,PB,G) ( All (a,PA,G) '<' a & a '<' Ex (a,PB,G) ) by BVFUNC_2:11, BVFUNC_2:12; hence All (a,PA,G) '<' Ex (a,PB,G) by BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC_4:18 for Y being non empty set for a, u being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st a 'imp' u = I_el Y holds (All (a,PA,G)) 'imp' u = I_el Y proof let Y be non empty set ; ::_thesis: for a, u being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st a 'imp' u = I_el Y holds (All (a,PA,G)) 'imp' u = I_el Y let a, u be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st a 'imp' u = I_el Y holds (All (a,PA,G)) 'imp' u = I_el Y let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st a 'imp' u = I_el Y holds (All (a,PA,G)) 'imp' u = I_el Y let PA be a_partition of Y; ::_thesis: ( a 'imp' u = I_el Y implies (All (a,PA,G)) 'imp' u = I_el Y ) assume A1: a 'imp' u = I_el Y ; ::_thesis: (All (a,PA,G)) 'imp' u = I_el Y for x being Element of Y holds ((All (a,PA,G)) 'imp' u) . x = TRUE proof let x be Element of Y; ::_thesis: ((All (a,PA,G)) 'imp' u) . x = TRUE (a 'imp' u) . x = TRUE by A1, BVFUNC_1:def_11; then A2: ('not' (a . x)) 'or' (u . x) = TRUE by BVFUNC_1:def_8; A3: ( 'not' (a . x) = TRUE or 'not' (a . x) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_(a_._x)_=_TRUE_&_((All_(a,PA,G))_'imp'_u)_._x_=_TRUE_)_or_(_u_._x_=_TRUE_&_((All_(a,PA,G))_'imp'_u)_._x_=_TRUE_)_) percases ( 'not' (a . x) = TRUE or u . x = TRUE ) by A2, A3; caseA4: 'not' (a . x) = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' u) . x = TRUE x in EqClass (x,(CompF (PA,G))) by EQREL_1:def_6; then (B_INF (a,(CompF (PA,G)))) . x = FALSE by A4, BVFUNC_1:def_16; then ((All (a,PA,G)) 'imp' u) . x = TRUE 'or' (u . x) by BVFUNC_1:def_8 .= TRUE ; hence ((All (a,PA,G)) 'imp' u) . x = TRUE ; ::_thesis: verum end; case u . x = TRUE ; ::_thesis: ((All (a,PA,G)) 'imp' u) . x = TRUE then ((All (a,PA,G)) 'imp' u) . x = ('not' ((All (a,PA,G)) . x)) 'or' TRUE by BVFUNC_1:def_8 .= TRUE ; hence ((All (a,PA,G)) 'imp' u) . x = TRUE ; ::_thesis: verum end; end; end; hence ((All (a,PA,G)) 'imp' u) . x = TRUE ; ::_thesis: verum end; hence (All (a,PA,G)) 'imp' u = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_4:19 for Y being non empty set for u being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st u is_independent_of PA,G holds Ex (u,PA,G) '<' u proof let Y be non empty set ; ::_thesis: for u being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st u is_independent_of PA,G holds Ex (u,PA,G) '<' u let u be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st u is_independent_of PA,G holds Ex (u,PA,G) '<' u let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds Ex (u,PA,G) '<' u let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies Ex (u,PA,G) '<' u ) assume u is_independent_of PA,G ; ::_thesis: Ex (u,PA,G) '<' u then A1: u is_dependent_of CompF (PA,G) by BVFUNC_2:def_8; for z being Element of Y holds ((Ex (u,PA,G)) 'imp' u) . z = TRUE proof let z be Element of Y; ::_thesis: ((Ex (u,PA,G)) 'imp' u) . z = TRUE A2: ((Ex (u,PA,G)) 'imp' u) . z = ('not' ((Ex (u,PA,G)) . z)) 'or' (u . z) by BVFUNC_1:def_8; A3: ( z in EqClass (z,(CompF (PA,G))) & EqClass (z,(CompF (PA,G))) in CompF (PA,G) ) by EQREL_1:def_6; now__::_thesis:_(_(_u_._z_=_TRUE_&_((Ex_(u,PA,G))_'imp'_u)_._z_=_TRUE_)_or_(_u_._z_=_FALSE_&_((Ex_(u,PA,G))_'imp'_u)_._z_=_TRUE_)_) percases ( u . z = TRUE or u . z = FALSE ) by XBOOLEAN:def_3; case u . z = TRUE ; ::_thesis: ((Ex (u,PA,G)) 'imp' u) . z = TRUE hence ((Ex (u,PA,G)) 'imp' u) . z = TRUE by A2; ::_thesis: verum end; case u . z = FALSE ; ::_thesis: ((Ex (u,PA,G)) 'imp' u) . z = TRUE then for x1 being Element of Y holds ( not x1 in EqClass (z,(CompF (PA,G))) or not u . x1 = TRUE ) by A1, A3, BVFUNC_1:def_15; then (B_SUP (u,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17; hence ((Ex (u,PA,G)) 'imp' u) . z = TRUE by A2; ::_thesis: verum end; end; end; hence ((Ex (u,PA,G)) 'imp' u) . z = TRUE ; ::_thesis: verum end; then (Ex (u,PA,G)) 'imp' u = I_el Y by BVFUNC_1:def_11; hence Ex (u,PA,G) '<' u by BVFUNC_1:16; ::_thesis: verum end; theorem :: BVFUNC_4:20 for Y being non empty set for u being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st u is_independent_of PA,G holds u '<' All (u,PA,G) proof let Y be non empty set ; ::_thesis: for u being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st u is_independent_of PA,G holds u '<' All (u,PA,G) let u be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st u is_independent_of PA,G holds u '<' All (u,PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st u is_independent_of PA,G holds u '<' All (u,PA,G) let PA be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies u '<' All (u,PA,G) ) assume u is_independent_of PA,G ; ::_thesis: u '<' All (u,PA,G) then A1: u is_dependent_of CompF (PA,G) by BVFUNC_2:def_8; for z being Element of Y holds (u 'imp' (All (u,PA,G))) . z = TRUE proof let z be Element of Y; ::_thesis: (u 'imp' (All (u,PA,G))) . z = TRUE A2: (u 'imp' (All (u,PA,G))) . z = ('not' (u . z)) 'or' ((All (u,PA,G)) . z) by BVFUNC_1:def_8; A3: ( z in EqClass (z,(CompF (PA,G))) & EqClass (z,(CompF (PA,G))) in CompF (PA,G) ) by EQREL_1:def_6; now__::_thesis:_(_(_u_._z_=_FALSE_&_(u_'imp'_(All_(u,PA,G)))_._z_=_TRUE_)_or_(_u_._z_=_TRUE_&_(u_'imp'_(All_(u,PA,G)))_._z_=_TRUE_)_) percases ( u . z = FALSE or u . z = TRUE ) by XBOOLEAN:def_3; case u . z = FALSE ; ::_thesis: (u 'imp' (All (u,PA,G))) . z = TRUE hence (u 'imp' (All (u,PA,G))) . z = TRUE by A2; ::_thesis: verum end; case u . z = TRUE ; ::_thesis: (u 'imp' (All (u,PA,G))) . z = TRUE then for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds u . x = TRUE by A1, A3, BVFUNC_1:def_15; then (All (u,PA,G)) . z = TRUE by BVFUNC_1:def_16; hence (u 'imp' (All (u,PA,G))) . z = TRUE by A2; ::_thesis: verum end; end; end; hence (u 'imp' (All (u,PA,G))) . z = TRUE ; ::_thesis: verum end; then u 'imp' (All (u,PA,G)) = I_el Y by BVFUNC_1:def_11; hence u '<' All (u,PA,G) by BVFUNC_1:16; ::_thesis: verum end; theorem :: BVFUNC_4:21 for Y being non empty set for u being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA, PB being a_partition of Y st u is_independent_of PB,G holds All (u,PA,G) '<' All (u,PB,G) proof let Y be non empty set ; ::_thesis: for u being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA, PB being a_partition of Y st u is_independent_of PB,G holds All (u,PA,G) '<' All (u,PB,G) let u be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA, PB being a_partition of Y st u is_independent_of PB,G holds All (u,PA,G) '<' All (u,PB,G) let G be Subset of (PARTITIONS Y); ::_thesis: for PA, PB being a_partition of Y st u is_independent_of PB,G holds All (u,PA,G) '<' All (u,PB,G) let PA, PB be a_partition of Y; ::_thesis: ( u is_independent_of PB,G implies All (u,PA,G) '<' All (u,PB,G) ) assume u is_independent_of PB,G ; ::_thesis: All (u,PA,G) '<' All (u,PB,G) then A1: u is_dependent_of CompF (PB,G) by BVFUNC_2:def_8; for z being Element of Y holds ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE proof let z be Element of Y; ::_thesis: ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE A2: ( z in EqClass (z,(CompF (PB,G))) & EqClass (z,(CompF (PB,G))) in CompF (PB,G) ) by EQREL_1:def_6; A3: ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = ('not' ((All (u,PA,G)) . z)) 'or' ((All (u,PB,G)) . z) by BVFUNC_1:def_8; A4: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; now__::_thesis:_(_(_(All_(u,PA,G))_._z_=_FALSE_&_((All_(u,PA,G))_'imp'_(All_(u,PB,G)))_._z_=_TRUE_)_or_(_(All_(u,PA,G))_._z_=_TRUE_&_((All_(u,PA,G))_'imp'_(All_(u,PB,G)))_._z_=_TRUE_)_) percases ( (All (u,PA,G)) . z = FALSE or (All (u,PA,G)) . z = TRUE ) by XBOOLEAN:def_3; case (All (u,PA,G)) . z = FALSE ; ::_thesis: ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE hence ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE by A3; ::_thesis: verum end; case (All (u,PA,G)) . z = TRUE ; ::_thesis: ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE then u . z = TRUE by A4, BVFUNC_1:def_16; then for x being Element of Y st x in EqClass (z,(CompF (PB,G))) holds u . x = TRUE by A1, A2, BVFUNC_1:def_15; then (All (u,PB,G)) . z = TRUE by BVFUNC_1:def_16; hence ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE by A3; ::_thesis: verum end; end; end; hence ((All (u,PA,G)) 'imp' (All (u,PB,G))) . z = TRUE ; ::_thesis: verum end; then (All (u,PA,G)) 'imp' (All (u,PB,G)) = I_el Y by BVFUNC_1:def_11; hence All (u,PA,G) '<' All (u,PB,G) by BVFUNC_1:16; ::_thesis: verum end; theorem :: BVFUNC_4:22 for Y being non empty set for u being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA, PB being a_partition of Y st u is_independent_of PA,G holds Ex (u,PA,G) '<' Ex (u,PB,G) proof let Y be non empty set ; ::_thesis: for u being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA, PB being a_partition of Y st u is_independent_of PA,G holds Ex (u,PA,G) '<' Ex (u,PB,G) let u be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA, PB being a_partition of Y st u is_independent_of PA,G holds Ex (u,PA,G) '<' Ex (u,PB,G) let G be Subset of (PARTITIONS Y); ::_thesis: for PA, PB being a_partition of Y st u is_independent_of PA,G holds Ex (u,PA,G) '<' Ex (u,PB,G) let PA, PB be a_partition of Y; ::_thesis: ( u is_independent_of PA,G implies Ex (u,PA,G) '<' Ex (u,PB,G) ) assume u is_independent_of PA,G ; ::_thesis: Ex (u,PA,G) '<' Ex (u,PB,G) then A1: u is_dependent_of CompF (PA,G) by BVFUNC_2:def_8; for z being Element of Y holds ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE proof let z be Element of Y; ::_thesis: ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE A2: z in EqClass (z,(CompF (PB,G))) by EQREL_1:def_6; A3: ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = ('not' ((Ex (u,PA,G)) . z)) 'or' ((Ex (u,PB,G)) . z) by BVFUNC_1:def_8; A4: ( z in EqClass (z,(CompF (PA,G))) & EqClass (z,(CompF (PA,G))) in CompF (PA,G) ) by EQREL_1:def_6; now__::_thesis:_(_(_(Ex_(u,PB,G))_._z_=_TRUE_&_((Ex_(u,PA,G))_'imp'_(Ex_(u,PB,G)))_._z_=_TRUE_)_or_(_(Ex_(u,PB,G))_._z_=_FALSE_&_((Ex_(u,PA,G))_'imp'_(Ex_(u,PB,G)))_._z_=_TRUE_)_) percases ( (Ex (u,PB,G)) . z = TRUE or (Ex (u,PB,G)) . z = FALSE ) by XBOOLEAN:def_3; case (Ex (u,PB,G)) . z = TRUE ; ::_thesis: ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE hence ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE by A3; ::_thesis: verum end; case (Ex (u,PB,G)) . z = FALSE ; ::_thesis: ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE then u . z <> TRUE by A2, BVFUNC_1:def_17; then for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not u . x = TRUE ) by A1, A4, BVFUNC_1:def_15; then (B_SUP (u,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17; hence ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE by A3; ::_thesis: verum end; end; end; hence ((Ex (u,PA,G)) 'imp' (Ex (u,PB,G))) . z = TRUE ; ::_thesis: verum end; then (Ex (u,PA,G)) 'imp' (Ex (u,PB,G)) = I_el Y by BVFUNC_1:def_11; hence Ex (u,PA,G) '<' Ex (u,PB,G) by BVFUNC_1:16; ::_thesis: verum end; theorem :: BVFUNC_4:23 for Y being non empty set for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) '<' (All (a,PA,G)) 'eqv' (All (b,PA,G)) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) '<' (All (a,PA,G)) 'eqv' (All (b,PA,G)) let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) '<' (All (a,PA,G)) 'eqv' (All (b,PA,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y holds All ((a 'eqv' b),PA,G) '<' (All (a,PA,G)) 'eqv' (All (b,PA,G)) let PA be a_partition of Y; ::_thesis: All ((a 'eqv' b),PA,G) '<' (All (a,PA,G)) 'eqv' (All (b,PA,G)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a 'eqv' b),PA,G)) . z = TRUE or ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE ) assume A1: (All ((a 'eqv' b),PA,G)) . z = TRUE ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE A2: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = 'not' (((All (a,PA,G)) . z) 'xor' ((All (b,PA,G)) . z)) by BVFUNC_1:def_9 .= ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ('not' ((All (a,PA,G)) . z))) 'or' ((((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z))) '&' ((All (b,PA,G)) . z)) by XBOOLEAN:8 .= ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) 'or' (((All (b,PA,G)) . z) '&' (((All (a,PA,G)) . z) 'or' ('not' ((All (b,PA,G)) . z)))) by XBOOLEAN:8 .= ((('not' ((All (a,PA,G)) . z)) '&' ((All (a,PA,G)) . z)) 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) 'or' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)))) by XBOOLEAN:8 .= (FALSE 'or' (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z)))) 'or' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' (((All (b,PA,G)) . z) '&' ('not' ((All (b,PA,G)) . z)))) by XBOOLEAN:138 .= (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) 'or' ((((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) 'or' FALSE) by XBOOLEAN:138 .= (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) ; percases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds b . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds b . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ) ; supposeA3: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE then (B_INF (b,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16; hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A2, A3, BVFUNC_1:def_16; ::_thesis: verum end; supposeA4: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE then consider x1 being Element of Y such that A5: x1 in EqClass (z,(CompF (PA,G))) and A6: b . x1 <> TRUE ; A7: a . x1 = TRUE by A4, A5; (a 'eqv' b) . x1 = 'not' ((a . x1) 'xor' (b . x1)) by BVFUNC_1:def_9 .= FALSE by A6, A7, XBOOLEAN:def_3 ; hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A1, A5, BVFUNC_1:def_16; ::_thesis: verum end; supposeA8: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE then consider x1 being Element of Y such that A9: x1 in EqClass (z,(CompF (PA,G))) and A10: a . x1 <> TRUE ; A11: b . x1 = TRUE by A8, A9; (a 'eqv' b) . x1 = 'not' ((a . x1) 'xor' (b . x1)) by BVFUNC_1:def_9 .= FALSE by A10, A11, XBOOLEAN:def_3 ; hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A1, A9, BVFUNC_1:def_16; ::_thesis: verum end; supposeA12: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ) ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE then (B_INF (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16; hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A2, A12, BVFUNC_1:def_16; ::_thesis: verum end; end; end; theorem :: BVFUNC_4:24 for Y being non empty set for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G)) proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G)) let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y holds All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G)) let PA be a_partition of Y; ::_thesis: All ((a '&' b),PA,G) '<' a '&' (All (b,PA,G)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((a '&' b),PA,G)) . z = TRUE or (a '&' (All (b,PA,G))) . z = TRUE ) assume A1: (All ((a '&' b),PA,G)) . z = TRUE ; ::_thesis: (a '&' (All (b,PA,G))) . z = TRUE A2: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_ a_._x_=_TRUE assume ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) ; ::_thesis: contradiction 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 = TRUE by A1, A3, BVFUNC_1:def_16; then A5: (a . x1) '&' (b . x1) = TRUE by MARGREL1:def_20; a . x1 = FALSE by A4, XBOOLEAN:def_3; hence contradiction by A5; ::_thesis: verum end; now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_ b_._x_=_TRUE assume ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; ::_thesis: contradiction then consider x1 being Element of Y such that A6: x1 in EqClass (z,(CompF (PA,G))) and A7: b . x1 <> TRUE ; (a '&' b) . x1 = TRUE by A1, A6, BVFUNC_1:def_16; then A8: (a . x1) '&' (b . x1) = TRUE by MARGREL1:def_20; b . x1 = FALSE by A7, XBOOLEAN:def_3; hence contradiction by A8; ::_thesis: verum end; then A9: (B_INF (b,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_16; z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; then a . z = TRUE by A2; then (a '&' (All (b,PA,G))) . z = TRUE '&' TRUE by A9, MARGREL1:def_20 .= TRUE ; hence (a '&' (All (b,PA,G))) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC_4:25 for Y being non empty set for a, u being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds (All (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G) proof let Y be non empty set ; ::_thesis: for a, u being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds (All (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G) let a, u be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA being a_partition of Y holds (All (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G) let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y holds (All (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G) let PA be a_partition of Y; ::_thesis: (All (a,PA,G)) 'imp' u '<' Ex ((a 'imp' u),PA,G) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((All (a,PA,G)) 'imp' u) . z = TRUE or (Ex ((a 'imp' u),PA,G)) . z = TRUE ) A1: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def_6; assume ((All (a,PA,G)) 'imp' u) . z = TRUE ; ::_thesis: (Ex ((a 'imp' u),PA,G)) . z = TRUE then A2: ('not' ((All (a,PA,G)) . z)) 'or' (u . z) = TRUE by BVFUNC_1:def_8; A3: ( 'not' ((All (a,PA,G)) . z) = TRUE or 'not' ((All (a,PA,G)) . z) = FALSE ) by XBOOLEAN:def_3; now__::_thesis:_(_(_'not'_((All_(a,PA,G))_._z)_=_TRUE_&_(Ex_((a_'imp'_u),PA,G))_._z_=_TRUE_)_or_(_u_._z_=_TRUE_&_(Ex_((a_'imp'_u),PA,G))_._z_=_TRUE_)_) percases ( 'not' ((All (a,PA,G)) . z) = TRUE or u . z = TRUE ) by A2, A3; case 'not' ((All (a,PA,G)) . z) = TRUE ; ::_thesis: (Ex ((a 'imp' u),PA,G)) . z = TRUE then consider x1 being Element of Y such that A4: x1 in EqClass (z,(CompF (PA,G))) and A5: a . x1 <> TRUE by BVFUNC_1:def_16; now__::_thesis:_ex_x_being_Element_of_Y_st_ (_x_in_EqClass_(z,(CompF_(PA,G)))_&_(a_'imp'_u)_._x_=_TRUE_) assume for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not (a 'imp' u) . x = TRUE ) ; ::_thesis: contradiction then (a 'imp' u) . x1 <> TRUE by A4; then (a 'imp' u) . x1 = FALSE by XBOOLEAN:def_3; then A6: ('not' (a . x1)) 'or' (u . x1) = FALSE by BVFUNC_1:def_8; ( 'not' (a . x1) = TRUE or 'not' (a . x1) = FALSE ) by XBOOLEAN:def_3; hence contradiction by A5, A6; ::_thesis: verum end; hence (Ex ((a 'imp' u),PA,G)) . z = TRUE by BVFUNC_1:def_17; ::_thesis: verum end; caseA7: u . z = TRUE ; ::_thesis: (Ex ((a 'imp' u),PA,G)) . z = TRUE now__::_thesis:_ex_x_being_Element_of_Y_st_ (_x_in_EqClass_(z,(CompF_(PA,G)))_&_(a_'imp'_u)_._x_=_TRUE_) assume for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not (a 'imp' u) . x = TRUE ) ; ::_thesis: contradiction then (a 'imp' u) . z <> TRUE by A1; then (a 'imp' u) . z = FALSE by XBOOLEAN:def_3; then ('not' (a . z)) 'or' (u . z) = FALSE by BVFUNC_1:def_8; hence contradiction by A7; ::_thesis: verum end; hence (Ex ((a 'imp' u),PA,G)) . z = TRUE by BVFUNC_1:def_17; ::_thesis: verum end; end; end; hence (Ex ((a 'imp' u),PA,G)) . z = TRUE ; ::_thesis: verum end; theorem :: BVFUNC_4:26 for Y being non empty set for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st a 'eqv' b = I_el Y holds (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st a 'eqv' b = I_el Y holds (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st a 'eqv' b = I_el Y holds (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st a 'eqv' b = I_el Y holds (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y let PA be a_partition of Y; ::_thesis: ( a 'eqv' b = I_el Y implies (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y ) assume A1: a 'eqv' b = I_el Y ; ::_thesis: (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y then b 'imp' a = I_el Y by Th10; then A2: ('not' b) 'or' a = I_el Y by Th8; a 'imp' b = I_el Y by A1, Th10; then A3: ('not' a) 'or' b = I_el Y by Th8; for z being Element of Y holds ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE proof let z be Element of Y; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE A4: now__::_thesis:_(_(_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_ a_._x_=_TRUE_)_&_ex_x_being_Element_of_Y_st_ (_x_in_EqClass_(z,(CompF_(PA,G)))_&_not_b_._x_=_TRUE_)_implies_((All_(a,PA,G))_'eqv'_(All_(b,PA,G)))_._z_=_TRUE_) assume that A5: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE and A6: ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE consider x1 being Element of Y such that A7: x1 in EqClass (z,(CompF (PA,G))) and A8: b . x1 <> TRUE by A6; A9: a . x1 = TRUE by A5, A7; A10: b . x1 = FALSE by A8, XBOOLEAN:def_3; (('not' a) 'or' b) . x1 = (('not' a) . x1) 'or' (b . x1) by BVFUNC_1:def_4 .= FALSE 'or' FALSE by A10, A9, MARGREL1:def_19 .= FALSE ; hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A3, BVFUNC_1:def_11; ::_thesis: verum end; A11: now__::_thesis:_(_ex_x_being_Element_of_Y_st_ (_x_in_EqClass_(z,(CompF_(PA,G)))_&_not_a_._x_=_TRUE_)_&_(_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_ b_._x_=_TRUE_)_implies_((All_(a,PA,G))_'eqv'_(All_(b,PA,G)))_._z_=_TRUE_) assume that A12: ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) and A13: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds b . x = TRUE ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE consider x1 being Element of Y such that A14: x1 in EqClass (z,(CompF (PA,G))) and A15: a . x1 <> TRUE by A12; A16: b . x1 = TRUE by A13, A14; A17: a . x1 = FALSE by A15, XBOOLEAN:def_3; (('not' b) 'or' a) . x1 = (('not' b) . x1) 'or' (a . x1) by BVFUNC_1:def_4 .= FALSE 'or' FALSE by A17, A16, MARGREL1:def_19 .= FALSE ; hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A2, BVFUNC_1:def_11; ::_thesis: verum end; (All (a,PA,G)) 'eqv' (All (b,PA,G)) = ((All (a,PA,G)) 'imp' (All (b,PA,G))) '&' ((All (b,PA,G)) 'imp' (All (a,PA,G))) by Th7 .= (('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' ((All (b,PA,G)) 'imp' (All (a,PA,G))) by Th8 .= (('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' (('not' (All (b,PA,G))) 'or' (All (a,PA,G))) by Th8 .= ((('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' (All (a,PA,G))) by BVFUNC_1:12 .= ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((All (b,PA,G)) '&' ('not' (All (b,PA,G))))) 'or' ((('not' (All (a,PA,G))) 'or' (All (b,PA,G))) '&' (All (a,PA,G))) by BVFUNC_1:12 .= ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((All (b,PA,G)) '&' ('not' (All (b,PA,G))))) 'or' ((('not' (All (a,PA,G))) '&' (All (a,PA,G))) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) by BVFUNC_1:12 .= ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' (O_el Y)) 'or' ((('not' (All (a,PA,G))) '&' (All (a,PA,G))) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) by Th5 .= ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' (O_el Y)) 'or' ((O_el Y) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) by Th5 .= (('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((O_el Y) 'or' ((All (b,PA,G)) '&' (All (a,PA,G)))) by BVFUNC_1:9 .= (('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) 'or' ((All (b,PA,G)) '&' (All (a,PA,G))) by BVFUNC_1:9 ; then A18: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = ((('not' (All (a,PA,G))) '&' ('not' (All (b,PA,G)))) . z) 'or' (((All (b,PA,G)) '&' (All (a,PA,G))) . z) by BVFUNC_1:def_4 .= ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z)) 'or' (((All (b,PA,G)) '&' (All (a,PA,G))) . z) by MARGREL1:def_20 .= ((('not' (All (a,PA,G))) . z) '&' (('not' (All (b,PA,G))) . z)) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) by MARGREL1:def_20 .= (('not' ((All (a,PA,G)) . z)) '&' (('not' (All (b,PA,G))) . z)) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) by MARGREL1:def_19 .= (('not' ((All (a,PA,G)) . z)) '&' ('not' ((All (b,PA,G)) . z))) 'or' (((All (b,PA,G)) . z) '&' ((All (a,PA,G)) . z)) by MARGREL1:def_19 ; A19: now__::_thesis:_(_ex_x_being_Element_of_Y_st_ (_x_in_EqClass_(z,(CompF_(PA,G)))_&_not_a_._x_=_TRUE_)_&_ex_x_being_Element_of_Y_st_ (_x_in_EqClass_(z,(CompF_(PA,G)))_&_not_b_._x_=_TRUE_)_implies_((All_(a,PA,G))_'eqv'_(All_(b,PA,G)))_._z_=_TRUE_) assume that A20: ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) and A21: ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & not b . x = TRUE ) ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE (B_INF (b,(CompF (PA,G)))) . z = FALSE by A21, BVFUNC_1:def_16; hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A18, A20, BVFUNC_1:def_16; ::_thesis: verum end; now__::_thesis:_(_(_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_ a_._x_=_TRUE_)_&_(_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_ b_._x_=_TRUE_)_implies_((All_(a,PA,G))_'eqv'_(All_(b,PA,G)))_._z_=_TRUE_) assume that A22: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds a . x = TRUE and A23: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds b . x = TRUE ; ::_thesis: ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE (B_INF (b,(CompF (PA,G)))) . z = TRUE by A23, BVFUNC_1:def_16; hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A18, A22, BVFUNC_1:def_16; ::_thesis: verum end; hence ((All (a,PA,G)) 'eqv' (All (b,PA,G))) . z = TRUE by A4, A11, A19; ::_thesis: verum end; hence (All (a,PA,G)) 'eqv' (All (b,PA,G)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end; theorem :: BVFUNC_4:27 for Y being non empty set for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st a 'eqv' b = I_el Y holds (Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y proof let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st a 'eqv' b = I_el Y holds (Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for PA being a_partition of Y st a 'eqv' b = I_el Y holds (Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y st a 'eqv' b = I_el Y holds (Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y let PA be a_partition of Y; ::_thesis: ( a 'eqv' b = I_el Y implies (Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y ) assume A1: a 'eqv' b = I_el Y ; ::_thesis: (Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y then b 'imp' a = I_el Y by Th10; then A2: ('not' b) 'or' a = I_el Y by Th8; a 'imp' b = I_el Y by A1, Th10; then A3: ('not' a) 'or' b = I_el Y by Th8; for z being Element of Y holds ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE proof let z be Element of Y; ::_thesis: ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE (Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = ((Ex (a,PA,G)) 'imp' (Ex (b,PA,G))) '&' ((Ex (b,PA,G)) 'imp' (Ex (a,PA,G))) by Th7 .= (('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' ((Ex (b,PA,G)) 'imp' (Ex (a,PA,G))) by Th8 .= (('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' (('not' (Ex (b,PA,G))) 'or' (Ex (a,PA,G))) by Th8 .= ((('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' (Ex (a,PA,G))) by BVFUNC_1:12 .= ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((Ex (b,PA,G)) '&' ('not' (Ex (b,PA,G))))) 'or' ((('not' (Ex (a,PA,G))) 'or' (Ex (b,PA,G))) '&' (Ex (a,PA,G))) by BVFUNC_1:12 .= ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((Ex (b,PA,G)) '&' ('not' (Ex (b,PA,G))))) 'or' ((('not' (Ex (a,PA,G))) '&' (Ex (a,PA,G))) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G)))) by BVFUNC_1:12 .= ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' (O_el Y)) 'or' ((('not' (Ex (a,PA,G))) '&' (Ex (a,PA,G))) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G)))) by Th5 .= ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' (O_el Y)) 'or' ((O_el Y) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G)))) by Th5 .= (('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((O_el Y) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G)))) by BVFUNC_1:9 .= (('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) 'or' ((Ex (b,PA,G)) '&' (Ex (a,PA,G))) by BVFUNC_1:9 ; then A4: ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = ((('not' (Ex (a,PA,G))) '&' ('not' (Ex (b,PA,G)))) . z) 'or' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z) by BVFUNC_1:def_4 .= ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z)) 'or' (((Ex (b,PA,G)) '&' (Ex (a,PA,G))) . z) by MARGREL1:def_20 .= ((('not' (Ex (a,PA,G))) . z) '&' (('not' (Ex (b,PA,G))) . z)) 'or' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)) by MARGREL1:def_20 .= (('not' ((Ex (a,PA,G)) . z)) '&' (('not' (Ex (b,PA,G))) . z)) 'or' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)) by MARGREL1:def_19 .= (('not' ((Ex (a,PA,G)) . z)) '&' ('not' ((Ex (b,PA,G)) . z))) 'or' (((Ex (b,PA,G)) . z) '&' ((Ex (a,PA,G)) . z)) by MARGREL1:def_19 ; percases ( ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & b . x = TRUE ) ) or ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ) ) or ( ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & b . x = TRUE ) ) or ( ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ) ) ) ; supposeA5: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & b . x = TRUE ) ) ; ::_thesis: ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE then (B_SUP (b,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def_17; hence ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE by A4, A5, BVFUNC_1:def_17; ::_thesis: verum end; supposeA6: ( ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ) ) ; ::_thesis: ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE then consider x1 being Element of Y such that A7: x1 in EqClass (z,(CompF (PA,G))) and A8: a . x1 = TRUE ; b . x1 <> TRUE by A6, A7; then A9: b . x1 = FALSE by XBOOLEAN:def_3; (('not' a) 'or' b) . x1 = (('not' a) . x1) 'or' (b . x1) by BVFUNC_1:def_4 .= FALSE 'or' FALSE by A8, A9, MARGREL1:def_19 .= FALSE ; hence ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE by A3, BVFUNC_1:def_11; ::_thesis: verum end; supposeA10: ( ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) & ex x being Element of Y st ( x in EqClass (z,(CompF (PA,G))) & b . x = TRUE ) ) ; ::_thesis: ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE then consider x1 being Element of Y such that A11: x1 in EqClass (z,(CompF (PA,G))) and A12: b . x1 = TRUE ; a . x1 <> TRUE by A10, A11; then A13: a . x1 = FALSE by XBOOLEAN:def_3; (('not' b) 'or' a) . x1 = (('not' b) . x1) 'or' (a . x1) by BVFUNC_1:def_4 .= FALSE 'or' FALSE by A12, A13, MARGREL1:def_19 .= FALSE ; hence ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE by A2, BVFUNC_1:def_11; ::_thesis: verum end; supposeA14: ( ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) & ( for x being Element of Y holds ( not x in EqClass (z,(CompF (PA,G))) or not b . x = TRUE ) ) ) ; ::_thesis: ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE then (B_SUP (b,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_17; hence ((Ex (a,PA,G)) 'eqv' (Ex (b,PA,G))) . z = TRUE by A4, A14, BVFUNC_1:def_17; ::_thesis: verum end; end; end; hence (Ex (a,PA,G)) 'eqv' (Ex (b,PA,G)) = I_el Y by BVFUNC_1:def_11; ::_thesis: verum end;