:: BVFUNC11 semantic presentation begin theorem Th1: :: BVFUNC11:1 for Y being non empty set for z being Element of Y for PA, PB being a_partition of Y st PA '<' PB holds EqClass (z,PA) c= EqClass (z,PB) proof let Y be non empty set ; ::_thesis: for z being Element of Y for PA, PB being a_partition of Y st PA '<' PB holds EqClass (z,PA) c= EqClass (z,PB) let z be Element of Y; ::_thesis: for PA, PB being a_partition of Y st PA '<' PB holds EqClass (z,PA) c= EqClass (z,PB) let PA, PB be a_partition of Y; ::_thesis: ( PA '<' PB implies EqClass (z,PA) c= EqClass (z,PB) ) assume PA '<' PB ; ::_thesis: EqClass (z,PA) c= EqClass (z,PB) then A1: ex b being set st ( b in PB & EqClass (z,PA) c= b ) by SETFAM_1:def_2; z in EqClass (z,PA) by EQREL_1:def_6; hence EqClass (z,PA) c= EqClass (z,PB) by A1, EQREL_1:def_6; ::_thesis: verum end; theorem :: BVFUNC11:2 for Y being non empty set for z being Element of Y for PA, PB being a_partition of Y holds EqClass (z,PA) c= EqClass (z,(PA '\/' PB)) by Th1, PARTIT1:16; theorem :: BVFUNC11:3 for Y being non empty set for z being Element of Y for PA, PB being a_partition of Y holds EqClass (z,(PA '/\' PB)) c= EqClass (z,PA) by Th1, PARTIT1:15; theorem :: BVFUNC11:4 for Y being non empty set for z being Element of Y for PA being a_partition of Y holds ( EqClass (z,PA) c= EqClass (z,(%O Y)) & EqClass (z,(%I Y)) c= EqClass (z,PA) ) by Th1, PARTIT1:32; theorem :: BVFUNC11:5 for Y being non empty set for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent & G = {A,B} & A <> B holds for a, b being set st a in A & b in B holds a meets b proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent & G = {A,B} & A <> B holds for a, b being set st a in A & b in B holds a meets b let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent & G = {A,B} & A <> B holds for a, b being set st a in A & b in B holds a meets b let A, B be a_partition of Y; ::_thesis: ( G is independent & G = {A,B} & A <> B implies for a, b being set st a in A & b in B holds a meets b ) assume that A1: G is independent and A2: G = {A,B} and A3: A <> B ; ::_thesis: for a, b being set st a in A & b in B holds a meets b let a, b be set ; ::_thesis: ( a in A & b in B implies a meets b ) assume that A4: a in A and A5: b in B ; ::_thesis: a meets b set h2 = (A,B) --> (a,b); A6: for d being set st d in G holds ((A,B) --> (a,b)) . d in d proof let d be set ; ::_thesis: ( d in G implies ((A,B) --> (a,b)) . d in d ) assume d in G ; ::_thesis: ((A,B) --> (a,b)) . d in d then ( d = A or d = B ) by A2, TARSKI:def_2; hence ((A,B) --> (a,b)) . d in d by A3, A4, A5, FUNCT_4:63; ::_thesis: verum end; {a,b} c= bool Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a,b} or x in bool Y ) assume x in {a,b} ; ::_thesis: x in bool Y then ( x = a or x = b ) by TARSKI:def_2; hence x in bool Y by A4, A5; ::_thesis: verum end; then reconsider SS = {a,b} as Subset-Family of Y ; A7: dom ((A,B) --> (a,b)) = {A,B} by FUNCT_4:62; rng ((A,B) --> (a,b)) = SS by A3, FUNCT_4:64; then Intersect SS <> {} by A1, A2, A7, A6, BVFUNC_2:def_5; hence a /\ b <> {} by A4, A5, MSSUBFAM:10; :: according to XBOOLE_0:def_7 ::_thesis: verum end; theorem :: BVFUNC11:6 for Y being non empty set for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent & G = {A,B} & A <> B holds '/\' G = A '/\' B proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent & G = {A,B} & A <> B holds '/\' G = A '/\' B let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent & G = {A,B} & A <> B holds '/\' G = A '/\' B let A, B be a_partition of Y; ::_thesis: ( G is independent & G = {A,B} & A <> B implies '/\' G = A '/\' B ) assume that A1: G is independent and A2: G = {A,B} and A3: A <> B ; ::_thesis: '/\' G = A '/\' B A4: '/\' G c= A '/\' B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in '/\' G or x in A '/\' B ) assume x in '/\' G ; ::_thesis: x in A '/\' B then consider h being Function, F being Subset-Family of Y such that A5: dom h = G and A6: rng h = F and A7: for d being set st d in G holds h . d in d and A8: x = Intersect F and A9: x <> {} by BVFUNC_2:def_1; A10: not x in {{}} by A9, TARSKI:def_1; A11: A in G by A2, TARSKI:def_2; then A12: h . A in rng h by A5, FUNCT_1:def_3; then A13: Intersect F = meet (rng h) by A6, SETFAM_1:def_9; A14: (h . A) /\ (h . B) c= x proof A15: rng h = {(h . A),(h . B)} proof thus rng h c= {(h . A),(h . B)} :: according to XBOOLE_0:def_10 ::_thesis: {(h . A),(h . B)} c= rng h proof let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in rng h or m in {(h . A),(h . B)} ) assume m in rng h ; ::_thesis: m in {(h . A),(h . B)} then consider w being set such that A16: w in dom h and A17: m = h . w by FUNCT_1:def_3; ( w = A or w = B ) by A2, A5, A16, TARSKI:def_2; hence m in {(h . A),(h . B)} by A17, TARSKI:def_2; ::_thesis: verum end; let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in {(h . A),(h . B)} or m in rng h ) assume m in {(h . A),(h . B)} ; ::_thesis: m in rng h then A18: ( m = h . A or m = h . B ) by TARSKI:def_2; A19: B in dom h by A2, A5, TARSKI:def_2; A in dom h by A2, A5, TARSKI:def_2; hence m in rng h by A18, A19, FUNCT_1:def_3; ::_thesis: verum end; let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in (h . A) /\ (h . B) or m in x ) assume A20: m in (h . A) /\ (h . B) ; ::_thesis: m in x then A21: m in h . B by XBOOLE_0:def_4; m in h . A by A20, XBOOLE_0:def_4; then for y being set st y in rng h holds m in y by A21, A15, TARSKI:def_2; hence m in x by A8, A12, A13, SETFAM_1:def_1; ::_thesis: verum end; A22: B in G by A2, TARSKI:def_2; then A23: h . B in B by A7; A24: h . B in rng h by A5, A22, FUNCT_1:def_3; x c= (h . A) /\ (h . B) proof let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in x or m in (h . A) /\ (h . B) ) assume A25: m in x ; ::_thesis: m in (h . A) /\ (h . B) then A26: m in h . B by A8, A24, A13, SETFAM_1:def_1; m in h . A by A8, A12, A13, A25, SETFAM_1:def_1; hence m in (h . A) /\ (h . B) by A26, XBOOLE_0:def_4; ::_thesis: verum end; then A27: (h . A) /\ (h . B) = x by A14, XBOOLE_0:def_10; h . A in A by A7, A11; then x in INTERSECTION (A,B) by A23, A27, SETFAM_1:def_5; then x in (INTERSECTION (A,B)) \ {{}} by A10, XBOOLE_0:def_5; hence x in A '/\' B by PARTIT1:def_4; ::_thesis: verum end; A '/\' B c= '/\' G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A '/\' B or x in '/\' G ) assume x in A '/\' B ; ::_thesis: x in '/\' G then x in (INTERSECTION (A,B)) \ {{}} by PARTIT1:def_4; then consider X, Z being set such that A28: X in A and A29: Z in B and A30: x = X /\ Z by SETFAM_1:def_5; {X,Z} c= bool Y proof let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in {X,Z} or m in bool Y ) assume m in {X,Z} ; ::_thesis: m in bool Y then ( m = X or m = Z ) by TARSKI:def_2; hence m in bool Y by A28, A29; ::_thesis: verum end; then reconsider SS = {X,Z} as Subset-Family of Y ; A31: X /\ Z = Intersect SS by A28, A29, MSSUBFAM:10; set h = (A,B) --> (X,Z); A32: for d being set st d in G holds ((A,B) --> (X,Z)) . d in d proof let d be set ; ::_thesis: ( d in G implies ((A,B) --> (X,Z)) . d in d ) assume d in G ; ::_thesis: ((A,B) --> (X,Z)) . d in d then ( d = A or d = B ) by A2, TARSKI:def_2; hence ((A,B) --> (X,Z)) . d in d by A3, A28, A29, FUNCT_4:63; ::_thesis: verum end; A33: dom ((A,B) --> (X,Z)) = {A,B} by FUNCT_4:62; A34: rng ((A,B) --> (X,Z)) = SS by A3, FUNCT_4:64; then Intersect SS <> {} by A1, A2, A33, A32, BVFUNC_2:def_5; hence x in '/\' G by A2, A30, A33, A34, A32, A31, BVFUNC_2:def_1; ::_thesis: verum end; hence '/\' G = A '/\' B by A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: BVFUNC11:7 for Y being non empty set for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G = {A,B} & A <> B holds CompF (A,G) = B proof let Y be non empty set ; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G = {A,B} & A <> B holds CompF (A,G) = B let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G = {A,B} & A <> B holds CompF (A,G) = B let A, B be a_partition of Y; ::_thesis: ( G = {A,B} & A <> B implies CompF (A,G) = B ) assume that A1: G = {A,B} and A2: A <> B ; ::_thesis: CompF (A,G) = B A3: '/\' {B} c= B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in '/\' {B} or x in B ) assume x in '/\' {B} ; ::_thesis: x in B then consider h being Function, F being Subset-Family of Y such that A4: dom h = {B} and A5: rng h = F and A6: for d being set st d in {B} holds h . d in d and A7: x = Intersect F and x <> {} by BVFUNC_2:def_1; rng h = {(h . B)} by A4, FUNCT_1:4; then A8: x = meet {(h . B)} by A5, A7, SETFAM_1:def_9; B in {B} by TARSKI:def_1; then h . B in B by A6; hence x in B by A8, SETFAM_1:10; ::_thesis: verum end; A9: B c= '/\' {B} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in '/\' {B} ) set h0 = B .--> x; A10: dom (B .--> x) = {B} by FUNCOP_1:13; assume A11: x in B ; ::_thesis: x in '/\' {B} A12: for d being set st d in {B} holds (B .--> x) . d in d proof let d be set ; ::_thesis: ( d in {B} implies (B .--> x) . d in d ) assume d in {B} ; ::_thesis: (B .--> x) . d in d then d = B by TARSKI:def_1; hence (B .--> x) . d in d by A11, FUNCOP_1:72; ::_thesis: verum end; A13: rng (B .--> x) = {x} by FUNCOP_1:8; rng (B .--> x) c= bool Y proof let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in rng (B .--> x) or m in bool Y ) assume m in rng (B .--> x) ; ::_thesis: m in bool Y then m = x by A13, TARSKI:def_1; hence m in bool Y by A11; ::_thesis: verum end; then reconsider F0 = rng (B .--> x) as Subset-Family of Y ; meet F0 = Intersect F0 by A13, SETFAM_1:def_9; then A14: x = Intersect F0 by A13, SETFAM_1:10; x <> {} by A11, EQREL_1:def_4; hence x in '/\' {B} by A10, A12, A14, BVFUNC_2:def_1; ::_thesis: verum end; A in {A} by TARSKI:def_1; then A15: {A} \ {A} = {} by ZFMISC_1:60; G \ {A} = ({A} \/ {B}) \ {A} by A1, ENUMSET1:1 .= ({A} \ {A}) \/ ({B} \ {A}) by XBOOLE_1:42 .= ({A} \ {A}) \/ {B} by A2, ZFMISC_1:14 ; then CompF (A,G) = '/\' {B} by A15, BVFUNC_2:def_7; hence CompF (A,G) = B by A3, A9, XBOOLE_0:def_10; ::_thesis: verum end; begin theorem Th8: :: BVFUNC11:8 for Y being non empty set for a, b being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A being a_partition of Y st a '<' b holds All (a,A,G) '<' Ex (b,A,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 A being a_partition of Y st a '<' b holds All (a,A,G) '<' Ex (b,A,G) let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A being a_partition of Y st a '<' b holds All (a,A,G) '<' Ex (b,A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A being a_partition of Y st a '<' b holds All (a,A,G) '<' Ex (b,A,G) let A be a_partition of Y; ::_thesis: ( a '<' b implies All (a,A,G) '<' Ex (b,A,G) ) assume a '<' b ; ::_thesis: All (a,A,G) '<' Ex (b,A,G) then A1: All (a,A,G) '<' All (b,A,G) by PARTIT_2:12; All (b,A,G) '<' Ex (b,A,G) by BVFUNC_4:17; hence All (a,A,G) '<' Ex (b,A,G) by A1, BVFUNC_1:15; ::_thesis: verum end; theorem Th9: :: BVFUNC11:9 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (a,A,G)),B,G) '<' Ex ((All (a,B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (a,A,G)),B,G) '<' Ex ((All (a,B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (a,A,G)),B,G) '<' Ex ((All (a,B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All ((All (a,A,G)),B,G) '<' Ex ((All (a,B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((All (a,A,G)),B,G) '<' Ex ((All (a,B,G)),A,G) ) assume G is independent ; ::_thesis: All ((All (a,A,G)),B,G) '<' Ex ((All (a,B,G)),A,G) then All ((All (a,A,G)),B,G) = All ((All (a,B,G)),A,G) by PARTIT_2:15; hence All ((All (a,A,G)),B,G) '<' Ex ((All (a,B,G)),A,G) by Th8; ::_thesis: verum end; theorem :: BVFUNC11:10 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) let A, B be a_partition of Y; ::_thesis: All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) A1: All ((All (a,A,G)),B,G) '<' All (a,A,G) by BVFUNC_2:11; All (a,A,G) '<' Ex ((Ex (a,B,G)),A,G) by Th8, BVFUNC_2:12; hence All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) by A1, BVFUNC_1:15; ::_thesis: verum end; theorem :: BVFUNC11:11 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (a,A,G)),B,G) '<' All ((Ex (a,B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (a,A,G)),B,G) '<' All ((Ex (a,B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (a,A,G)),B,G) '<' All ((Ex (a,B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All ((All (a,A,G)),B,G) '<' All ((Ex (a,B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((All (a,A,G)),B,G) '<' All ((Ex (a,B,G)),A,G) ) assume G is independent ; ::_thesis: All ((All (a,A,G)),B,G) '<' All ((Ex (a,B,G)),A,G) then A1: All ((All (a,A,G)),B,G) = All ((All (a,B,G)),A,G) by PARTIT_2:15; All (a,B,G) '<' Ex (a,B,G) by Th8; hence All ((All (a,A,G)),B,G) '<' All ((Ex (a,B,G)),A,G) by A1, PARTIT_2:12; ::_thesis: verum end; theorem :: BVFUNC11:12 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((Ex (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((Ex (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((Ex (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((Ex (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) let A, B be a_partition of Y; ::_thesis: All ((Ex (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) A1: Ex (a,B,G) = B_SUP (a,(CompF (B,G))) by BVFUNC_2:def_10; let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((Ex (a,A,G)),B,G)) . z = TRUE or (Ex ((Ex (a,B,G)),A,G)) . z = TRUE ) assume A2: (All ((Ex (a,A,G)),B,G)) . z = TRUE ; ::_thesis: (Ex ((Ex (a,B,G)),A,G)) . z = TRUE A3: now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(B,G)))_holds_ (Ex_(a,A,G))_._x_=_TRUE assume ex x being Element of Y st ( x in EqClass (z,(CompF (B,G))) & not (Ex (a,A,G)) . x = TRUE ) ; ::_thesis: contradiction then (B_INF ((Ex (a,A,G)),(CompF (B,G)))) . z = FALSE by BVFUNC_1:def_16; hence contradiction by A2, BVFUNC_2:def_9; ::_thesis: verum end; A4: z in EqClass (z,(CompF (B,G))) by EQREL_1:def_6; now__::_thesis:_ex_x_being_Element_of_Y_st_ (_x_in_EqClass_(z,(CompF_(A,G)))_&_a_._x_=_TRUE_) assume for x being Element of Y holds ( not x in EqClass (z,(CompF (A,G))) or not a . x = TRUE ) ; ::_thesis: contradiction then (B_SUP (a,(CompF (A,G)))) . z = FALSE by BVFUNC_1:def_17; then (Ex (a,A,G)) . z = FALSE by BVFUNC_2:def_10; hence contradiction by A4, A3; ::_thesis: verum end; then consider x1 being Element of Y such that A5: x1 in EqClass (z,(CompF (A,G))) and A6: a . x1 = TRUE ; x1 in EqClass (x1,(CompF (B,G))) by EQREL_1:def_6; then (Ex (a,B,G)) . x1 = TRUE by A1, A6, BVFUNC_1:def_17; then (B_SUP ((Ex (a,B,G)),(CompF (A,G)))) . z = TRUE by A5, BVFUNC_1:def_17; hence (Ex ((Ex (a,B,G)),A,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum end; theorem Th13: :: BVFUNC11:13 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) A1: All (a,A,G) = B_INF (a,(CompF (A,G))) by BVFUNC_2:def_9; let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ('not' (Ex ((All (a,A,G)),B,G))) . z = TRUE or (Ex ((Ex (('not' a),B,G)),A,G)) . z = TRUE ) A2: z in EqClass (z,(CompF (B,G))) by EQREL_1:def_6; assume ('not' (Ex ((All (a,A,G)),B,G))) . z = TRUE ; ::_thesis: (Ex ((Ex (('not' a),B,G)),A,G)) . z = TRUE then A3: 'not' ((Ex ((All (a,A,G)),B,G)) . z) = TRUE by MARGREL1:def_19; Ex ((All (a,A,G)),B,G) = B_SUP ((All (a,A,G)),(CompF (B,G))) by BVFUNC_2:def_10; then (All (a,A,G)) . z <> TRUE by A3, A2, BVFUNC_1:def_17; then consider x1 being Element of Y such that A4: x1 in EqClass (z,(CompF (A,G))) and A5: a . x1 <> TRUE by A1, BVFUNC_1:def_16; a . x1 = FALSE by A5, XBOOLEAN:def_3; then A6: ('not' a) . x1 = 'not' FALSE by MARGREL1:def_19; A7: Ex (('not' a),B,G) = B_SUP (('not' a),(CompF (B,G))) by BVFUNC_2:def_10; x1 in EqClass (x1,(CompF (B,G))) by EQREL_1:def_6; then (Ex (('not' a),B,G)) . x1 = TRUE by A7, A6, BVFUNC_1:def_17; then (B_SUP ((Ex (('not' a),B,G)),(CompF (A,G)))) . z = TRUE by A4, BVFUNC_1:def_17; hence (Ex ((Ex (('not' a),B,G)),A,G)) . z = TRUE by BVFUNC_2:def_10; ::_thesis: verum end; theorem Th14: :: BVFUNC11:14 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) ) assume G is independent ; ::_thesis: Ex (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) then Ex ((Ex (('not' a),B,G)),A,G) = Ex ((Ex (('not' a),A,G)),B,G) by PARTIT_2:16; hence Ex (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) by BVFUNC_2:18; ::_thesis: verum end; theorem Th15: :: BVFUNC11:15 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,B,G))),A,G) ) assume G is independent ; ::_thesis: 'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,B,G))),A,G) then All ((All (a,A,G)),B,G) = All ((All (a,B,G)),A,G) by PARTIT_2:15; hence 'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,B,G))),A,G) by BVFUNC_2:18; ::_thesis: verum end; theorem :: BVFUNC11:16 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) ) assume G is independent ; ::_thesis: All (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) then A1: Ex ((Ex (('not' a),B,G)),A,G) = Ex ((Ex (('not' a),A,G)),B,G) by PARTIT_2:16; 'not' (All (a,A,G)) = Ex (('not' a),A,G) by BVFUNC_2:18; hence All (('not' (All (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) by A1, Th8; ::_thesis: verum end; theorem :: BVFUNC11:17 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),B,G)),A,G) ) A1: Ex (('not' a),B,G) = 'not' (All (a,B,G)) by BVFUNC_2:18; assume G is independent ; ::_thesis: 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),B,G)),A,G) hence 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),B,G)),A,G) by A1, Th15; ::_thesis: verum end; theorem :: BVFUNC11:18 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),A,G)),B,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),A,G)),B,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),A,G)),B,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (All ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),A,G)),B,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),A,G)),B,G) ) assume A1: G is independent ; ::_thesis: 'not' (All ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),A,G)),B,G) then Ex (('not' (All (a,B,G))),A,G) '<' Ex ((Ex (('not' a),A,G)),B,G) by Th14; hence 'not' (All ((All (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),A,G)),B,G) by A1, Th15; ::_thesis: verum end; theorem Th19: :: BVFUNC11:19 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) let A, B be a_partition of Y; ::_thesis: 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) 'not' (All ((Ex (a,A,G)),B,G)) = Ex (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:18; hence 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) by BVFUNC_2:19; ::_thesis: verum end; theorem Th20: :: BVFUNC11:20 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G) let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G) 'not' (Ex ((All (a,A,G)),B,G)) = All (('not' (All (a,A,G))),B,G) by BVFUNC_2:19; hence 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G) by BVFUNC_2:18; ::_thesis: verum end; theorem Th21: :: BVFUNC11:21 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),A,G)),B,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),A,G)),B,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),A,G)),B,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),A,G)),B,G) let A, B be a_partition of Y; ::_thesis: 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),A,G)),B,G) Ex (('not' (All (a,A,G))),B,G) = Ex ((Ex (('not' a),A,G)),B,G) by BVFUNC_2:18; hence 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),A,G)),B,G) by BVFUNC_2:18; ::_thesis: verum end; theorem :: BVFUNC11:22 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) ) assume G is independent ; ::_thesis: Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) then A1: Ex ((Ex (a,B,G)),A,G) = Ex ((Ex (a,A,G)),B,G) by PARTIT_2:16; All (a,A,G) '<' Ex (a,A,G) by Th8; hence Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,B,G)),A,G) by A1, PARTIT_2:13; ::_thesis: verum end; theorem :: BVFUNC11:23 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G) let A, B be a_partition of Y; ::_thesis: All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G) All (a,A,G) '<' Ex (a,A,G) by Th8; hence All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G) by PARTIT_2:12; ::_thesis: verum end; theorem :: BVFUNC11:24 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) let A, B be a_partition of Y; ::_thesis: All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) All (a,A,G) '<' Ex (a,A,G) by Th8; hence All ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) by Th8; ::_thesis: verum end; theorem :: BVFUNC11:25 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) let A, B be a_partition of Y; ::_thesis: Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) All (a,A,G) '<' Ex (a,A,G) by Th8; hence Ex ((All (a,A,G)),B,G) '<' Ex ((Ex (a,A,G)),B,G) by PARTIT_2:13; ::_thesis: verum end; theorem Th26: :: BVFUNC11:26 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) ) assume G is independent ; ::_thesis: All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) then All ((All (a,B,G)),A,G) = All ((All (a,A,G)),B,G) by PARTIT_2:15; then ( All (('not' (All (a,A,G))),B,G) = 'not' (Ex ((All (a,A,G)),B,G)) & All ((All (a,B,G)),A,G) '<' Ex ((All (a,A,G)),B,G) ) by Th8, BVFUNC_2:19; hence All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by PARTIT_2:11; ::_thesis: verum end; theorem Th27: :: BVFUNC11:27 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All ((All (('not' a),A,G)),B,G)) . z = TRUE or ('not' (All ((All (a,B,G)),A,G))) . z = TRUE ) A1: z in EqClass (z,(CompF (A,G))) by EQREL_1:def_6; A2: z in EqClass (z,(CompF (B,G))) by EQREL_1:def_6; assume A3: (All ((All (('not' a),A,G)),B,G)) . z = TRUE ; ::_thesis: ('not' (All ((All (a,B,G)),A,G))) . z = TRUE now__::_thesis:_for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(B,G)))_holds_ (All_(('not'_a),A,G))_._x_=_TRUE assume ex x being Element of Y st ( x in EqClass (z,(CompF (B,G))) & not (All (('not' a),A,G)) . x = TRUE ) ; ::_thesis: contradiction then (B_INF ((All (('not' a),A,G)),(CompF (B,G)))) . z = FALSE by BVFUNC_1:def_16; hence contradiction by A3, BVFUNC_2:def_9; ::_thesis: verum end; then ( All (('not' a),A,G) = B_INF (('not' a),(CompF (A,G))) & (All (('not' a),A,G)) . z = TRUE ) by A2, BVFUNC_2:def_9; then ('not' a) . z = TRUE by A1, BVFUNC_1:def_16; then 'not' (a . z) = TRUE by MARGREL1:def_19; then (B_INF (a,(CompF (B,G)))) . z = FALSE by A2, BVFUNC_1:def_16; then (All (a,B,G)) . z = FALSE by BVFUNC_2:def_9; then (B_INF ((All (a,B,G)),(CompF (A,G)))) . z = FALSE by A1, BVFUNC_1:def_16; then (All ((All (a,B,G)),A,G)) . z = FALSE by BVFUNC_2:def_9; then 'not' ((All ((All (a,B,G)),A,G)) . z) = TRUE ; hence ('not' (All ((All (a,B,G)),A,G))) . z = TRUE by MARGREL1:def_19; ::_thesis: verum end; theorem Th28: :: BVFUNC11:28 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) by BVFUNC_2:19; hence All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by Th27; ::_thesis: verum end; theorem Th29: :: BVFUNC11:29 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((Ex (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((Ex (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((Ex (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All ((Ex (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((Ex (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) ) Ex (('not' a),A,G) = 'not' (All (a,A,G)) by BVFUNC_2:18; then A1: All ((Ex (('not' a),A,G)),B,G) = 'not' (Ex ((All (a,A,G)),B,G)) by BVFUNC_2:19; assume G is independent ; ::_thesis: All ((Ex (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) hence All ((Ex (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by A1, Th9, PARTIT_2:11; ::_thesis: verum end; theorem :: BVFUNC11:30 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) ) assume A1: G is independent ; ::_thesis: Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) then ( Ex ((All (('not' a),A,G)),B,G) '<' All ((Ex (('not' a),B,G)),A,G) & All ((Ex (('not' a),B,G)),A,G) '<' 'not' (All ((All (a,A,G)),B,G)) ) by Th29, PARTIT_2:17; then Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,A,G)),B,G)) by BVFUNC_1:15; hence Ex ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by A1, PARTIT_2:15; ::_thesis: verum end; theorem Th31: :: BVFUNC11:31 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) ) All (a,A,G) '<' Ex (a,A,G) by Th8; then A1: All ((All (a,A,G)),B,G) '<' All ((Ex (a,A,G)),B,G) by PARTIT_2:12; assume G is independent ; ::_thesis: Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) then ( Ex (('not' (Ex (a,A,G))),B,G) = 'not' (All ((Ex (a,A,G)),B,G)) & All ((All (a,B,G)),A,G) = All ((All (a,A,G)),B,G) ) by BVFUNC_2:18, PARTIT_2:15; hence Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by A1, PARTIT_2:11; ::_thesis: verum end; theorem :: BVFUNC11:32 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) by PARTIT_2:11, PARTIT_2:17; theorem Th33: :: BVFUNC11:33 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) ) assume G is independent ; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) then A1: Ex ((Ex (a,A,G)),B,G) = Ex ((Ex (a,B,G)),A,G) by PARTIT_2:16; All (a,B,G) '<' Ex (a,B,G) by Th8; then Ex ((All (a,B,G)),A,G) '<' Ex ((Ex (a,A,G)),B,G) by A1, PARTIT_2:13; hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) by PARTIT_2:11; ::_thesis: verum end; theorem Th34: :: BVFUNC11:34 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((Ex (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((Ex (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((Ex (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((Ex (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((Ex (a,B,G)),A,G)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ('not' (Ex ((Ex (a,A,G)),B,G))) . z = TRUE or ('not' (All ((Ex (a,B,G)),A,G))) . z = TRUE ) assume ('not' (Ex ((Ex (a,A,G)),B,G))) . z = TRUE ; ::_thesis: ('not' (All ((Ex (a,B,G)),A,G))) . z = TRUE then A1: 'not' ((Ex ((Ex (a,A,G)),B,G)) . z) = TRUE by MARGREL1:def_19; A2: now__::_thesis:_for_x_being_Element_of_Y_holds_ (_not_x_in_EqClass_(z,(CompF_(B,G)))_or_not_(Ex_(a,A,G))_._x_=_TRUE_) assume ex x being Element of Y st ( x in EqClass (z,(CompF (B,G))) & (Ex (a,A,G)) . x = TRUE ) ; ::_thesis: contradiction then (B_SUP ((Ex (a,A,G)),(CompF (B,G)))) . z = TRUE by BVFUNC_1:def_17; then (Ex ((Ex (a,A,G)),B,G)) . z = TRUE by BVFUNC_2:def_10; hence contradiction by A1; ::_thesis: verum end; A3: Ex (a,A,G) = B_SUP (a,(CompF (A,G))) by BVFUNC_2:def_10; A4: for x being Element of Y st x in EqClass (z,(CompF (B,G))) holds for y being Element of Y st y in EqClass (x,(CompF (A,G))) holds a . y <> TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (B,G))) implies for y being Element of Y st y in EqClass (x,(CompF (A,G))) holds a . y <> TRUE ) assume x in EqClass (z,(CompF (B,G))) ; ::_thesis: for y being Element of Y st y in EqClass (x,(CompF (A,G))) holds a . y <> TRUE then (Ex (a,A,G)) . x <> TRUE by A2; hence for y being Element of Y st y in EqClass (x,(CompF (A,G))) holds a . y <> TRUE by A3, BVFUNC_1:def_17; ::_thesis: verum end; for x being Element of Y st x in EqClass (z,(CompF (B,G))) holds a . x <> TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (B,G))) implies a . x <> TRUE ) A5: x in EqClass (x,(CompF (A,G))) by EQREL_1:def_6; assume x in EqClass (z,(CompF (B,G))) ; ::_thesis: a . x <> TRUE hence a . x <> TRUE by A4, A5; ::_thesis: verum end; then (B_SUP (a,(CompF (B,G)))) . z = FALSE by BVFUNC_1:def_17; then ( z in EqClass (z,(CompF (A,G))) & (Ex (a,B,G)) . z = FALSE ) by BVFUNC_2:def_10, EQREL_1:def_6; then (B_INF ((Ex (a,B,G)),(CompF (A,G)))) . z = FALSE by BVFUNC_1:def_16; then (All ((Ex (a,B,G)),A,G)) . z = FALSE by BVFUNC_2:def_9; then 'not' ((All ((Ex (a,B,G)),A,G)) . z) = TRUE ; hence ('not' (All ((Ex (a,B,G)),A,G))) . z = TRUE by MARGREL1:def_19; ::_thesis: verum end; theorem :: BVFUNC11:35 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((All (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((All (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((All (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (Ex ((All (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((All (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) ) assume G is independent ; ::_thesis: 'not' (Ex ((All (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) then All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by Th26; hence 'not' (Ex ((All (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) by BVFUNC_2:19; ::_thesis: verum end; theorem :: BVFUNC11:36 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) ) assume G is independent ; ::_thesis: 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) then A1: Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by Th31; Ex (('not' (Ex (a,A,G))),B,G) = Ex ((All (('not' a),A,G)),B,G) by BVFUNC_2:19; hence 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) by A1, Th19; ::_thesis: verum end; theorem :: BVFUNC11:37 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by Th28; hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((All (a,B,G)),A,G)) by BVFUNC_2:19; ::_thesis: verum end; theorem Th38: :: BVFUNC11:38 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) ) assume G is independent ; ::_thesis: 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) then A1: All (('not' (All (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by Th26; 'not' (Ex ((All (a,A,G)),B,G)) = All (('not' (All (a,A,G))),B,G) by BVFUNC_2:19; hence 'not' (Ex ((All (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) by A1, BVFUNC_2:18; ::_thesis: verum end; theorem Th39: :: BVFUNC11:39 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) ) assume G is independent ; ::_thesis: 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) then A1: Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) by Th31; ( 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) & Ex (('not' (Ex (a,A,G))),B,G) = Ex ((All (('not' a),A,G)),B,G) ) by Th19, BVFUNC_2:19; hence 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) by A1, BVFUNC_2:18; ::_thesis: verum end; theorem Th40: :: BVFUNC11:40 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) ( All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((All (a,B,G)),A,G)) & 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) ) by Th28, BVFUNC_2:19; hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) by BVFUNC_2:18; ::_thesis: verum end; theorem Th41: :: BVFUNC11:41 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) ) assume G is independent ; ::_thesis: 'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) then 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) by PARTIT_2:11, PARTIT_2:17; hence 'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) by BVFUNC_2:19; ::_thesis: verum end; theorem Th42: :: BVFUNC11:42 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) ) assume G is independent ; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) then 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) by Th33; hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) by BVFUNC_2:19; ::_thesis: verum end; theorem Th43: :: BVFUNC11:43 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (Ex (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (Ex (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (Ex (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (Ex (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (Ex (a,B,G))),A,G) ( 'not' (Ex ((Ex (a,A,G)),B,G)) '<' 'not' (All ((Ex (a,B,G)),A,G)) & Ex (('not' (Ex (a,B,G))),A,G) = Ex ((All (('not' a),B,G)),A,G) ) by Th34, BVFUNC_2:19; hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (Ex (a,B,G))),A,G) by Th19; ::_thesis: verum end; theorem Th44: :: BVFUNC11:44 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G) ) assume G is independent ; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G) then 'not' (Ex ((Ex (a,A,G)),B,G)) = 'not' (Ex ((Ex (a,B,G)),A,G)) by PARTIT_2:16; hence 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G) by BVFUNC_2:19; ::_thesis: verum end; theorem Th45: :: BVFUNC11:45 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) ) assume G is independent ; ::_thesis: 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) then 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) by Th39; hence 'not' (All ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) by BVFUNC_2:18; ::_thesis: verum end; theorem Th46: :: BVFUNC11:46 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (All (a,B,G))),A,G) by Th40; hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((Ex (('not' a),B,G)),A,G) by BVFUNC_2:18; ::_thesis: verum end; theorem Th47: :: BVFUNC11:47 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (All ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (All ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) ) assume G is independent ; ::_thesis: 'not' (All ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) then 'not' (All ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) by Th41; hence 'not' (All ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) by BVFUNC_2:18; ::_thesis: verum end; theorem Th48: :: BVFUNC11:48 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) ) assume G is independent ; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) then 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) by Th42; hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All ((Ex (('not' a),B,G)),A,G) by BVFUNC_2:18; ::_thesis: verum end; theorem Th49: :: BVFUNC11:49 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((All (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((All (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((All (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((All (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((All (('not' a),B,G)),A,G) 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex (('not' (Ex (a,B,G))),A,G) by Th43; hence 'not' (Ex ((Ex (a,A,G)),B,G)) '<' Ex ((All (('not' a),B,G)),A,G) by BVFUNC_2:19; ::_thesis: verum end; theorem Th50: :: BVFUNC11:50 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) = All ((All (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) = All ((All (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) = All ((All (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds 'not' (Ex ((Ex (a,A,G)),B,G)) = All ((All (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies 'not' (Ex ((Ex (a,A,G)),B,G)) = All ((All (('not' a),B,G)),A,G) ) assume G is independent ; ::_thesis: 'not' (Ex ((Ex (a,A,G)),B,G)) = All ((All (('not' a),B,G)),A,G) then 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,B,G))),A,G) by Th44; hence 'not' (Ex ((Ex (a,A,G)),B,G)) = All ((All (('not' a),B,G)),A,G) by BVFUNC_2:19; ::_thesis: verum end; theorem :: BVFUNC11:51 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) ) assume G is independent ; ::_thesis: Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) then A1: 'not' (All ((Ex (a,A,G)),B,G)) '<' 'not' (Ex ((All (a,B,G)),A,G)) by PARTIT_2:11, PARTIT_2:17; 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) by Th19; hence Ex (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) by A1, BVFUNC_2:19; ::_thesis: verum end; theorem :: BVFUNC11:52 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (All (('not' (Ex (a,A,G))),B,G)) . z = TRUE or ('not' (Ex ((All (a,B,G)),A,G))) . z = TRUE ) A1: ( All (('not' (Ex (a,A,G))),B,G) = B_INF (('not' (Ex (a,A,G))),(CompF (B,G))) & z in EqClass (z,(CompF (B,G))) ) by BVFUNC_2:def_9, EQREL_1:def_6; assume (All (('not' (Ex (a,A,G))),B,G)) . z = TRUE ; ::_thesis: ('not' (Ex ((All (a,B,G)),A,G))) . z = TRUE then ('not' (Ex (a,A,G))) . z = TRUE by A1, BVFUNC_1:def_16; then A2: ( Ex (a,A,G) = B_SUP (a,(CompF (A,G))) & 'not' ((Ex (a,A,G)) . z) = TRUE ) by BVFUNC_2:def_10, MARGREL1:def_19; A3: All (a,B,G) = B_INF (a,(CompF (B,G))) by BVFUNC_2:def_9; for x being Element of Y st x in EqClass (z,(CompF (A,G))) holds (All (a,B,G)) . x <> TRUE proof let x be Element of Y; ::_thesis: ( x in EqClass (z,(CompF (A,G))) implies (All (a,B,G)) . x <> TRUE ) assume x in EqClass (z,(CompF (A,G))) ; ::_thesis: (All (a,B,G)) . x <> TRUE then A4: a . x <> TRUE by A2, BVFUNC_1:def_17; x in EqClass (x,(CompF (B,G))) by EQREL_1:def_6; hence (All (a,B,G)) . x <> TRUE by A3, A4, BVFUNC_1:def_16; ::_thesis: verum end; then ( Ex ((All (a,B,G)),A,G) = B_SUP ((All (a,B,G)),(CompF (A,G))) & (B_SUP ((All (a,B,G)),(CompF (A,G)))) . z = FALSE ) by BVFUNC_1:def_17, BVFUNC_2:def_10; then 'not' ((Ex ((All (a,B,G)),A,G)) . z) = TRUE ; hence ('not' (Ex ((All (a,B,G)),A,G))) . z = TRUE by MARGREL1:def_19; ::_thesis: verum end; theorem :: BVFUNC11:53 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19; hence All (('not' (Ex (a,A,G))),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) by Th34; ::_thesis: verum end; theorem :: BVFUNC11:54 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) = 'not' (Ex ((Ex (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) = 'not' (Ex ((Ex (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) = 'not' (Ex ((Ex (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) = 'not' (Ex ((Ex (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (Ex (a,A,G))),B,G) = 'not' (Ex ((Ex (a,B,G)),A,G)) ) A1: 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19; assume G is independent ; ::_thesis: All (('not' (Ex (a,A,G))),B,G) = 'not' (Ex ((Ex (a,B,G)),A,G)) hence All (('not' (Ex (a,A,G))),B,G) = 'not' (Ex ((Ex (a,B,G)),A,G)) by A1, PARTIT_2:16; ::_thesis: verum end; theorem :: BVFUNC11:55 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (All (a,A,G))),B,G) = Ex (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (All (a,A,G))),B,G) = Ex (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (All (a,A,G))),B,G) = Ex (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex (('not' (All (a,A,G))),B,G) = Ex (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (All (a,A,G))),B,G) = Ex (('not' (All (a,B,G))),A,G) ) A1: 'not' (All ((All (a,A,G)),B,G)) = Ex (('not' (All (a,A,G))),B,G) by BVFUNC_2:18; assume G is independent ; ::_thesis: Ex (('not' (All (a,A,G))),B,G) = Ex (('not' (All (a,B,G))),A,G) hence Ex (('not' (All (a,A,G))),B,G) = Ex (('not' (All (a,B,G))),A,G) by A1, Th15; ::_thesis: verum end; theorem :: BVFUNC11:56 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (All (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (All (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (All (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All (('not' (All (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (All (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) ) A1: 'not' (Ex ((All (a,A,G)),B,G)) = All (('not' (All (a,A,G))),B,G) by BVFUNC_2:19; assume G is independent ; ::_thesis: All (('not' (All (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) hence All (('not' (All (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by A1, Th38; ::_thesis: verum end; theorem :: BVFUNC11:57 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) ) A1: ( 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) & Ex (('not' (Ex (a,A,G))),B,G) = Ex ((All (('not' a),A,G)),B,G) ) by Th19, BVFUNC_2:19; assume G is independent ; ::_thesis: Ex (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) hence Ex (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by A1, Th39; ::_thesis: verum end; theorem :: BVFUNC11:58 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19; hence All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by Th40; ::_thesis: verum end; theorem :: BVFUNC11:59 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) ) A1: ( 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) & Ex (('not' (Ex (a,A,G))),B,G) = Ex ((All (('not' a),A,G)),B,G) ) by Th19, BVFUNC_2:19; assume G is independent ; ::_thesis: Ex (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) hence Ex (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) by A1, Th41; ::_thesis: verum end; theorem :: BVFUNC11:60 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) ) assume G is independent ; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) then 'not' (Ex ((Ex (a,A,G)),B,G)) '<' All (('not' (All (a,B,G))),A,G) by Th42; hence All (('not' (Ex (a,A,G))),B,G) '<' All (('not' (All (a,B,G))),A,G) by BVFUNC_2:19; ::_thesis: verum end; theorem :: BVFUNC11:61 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19; hence All (('not' (Ex (a,A,G))),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) by Th43; ::_thesis: verum end; theorem :: BVFUNC11:62 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) = All (('not' (Ex (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) = All (('not' (Ex (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) = All (('not' (Ex (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) = All (('not' (Ex (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (Ex (a,A,G))),B,G) = All (('not' (Ex (a,B,G))),A,G) ) A1: 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19; assume G is independent ; ::_thesis: All (('not' (Ex (a,A,G))),B,G) = All (('not' (Ex (a,B,G))),A,G) hence All (('not' (Ex (a,A,G))),B,G) = All (('not' (Ex (a,B,G))),A,G) by A1, Th44; ::_thesis: verum end; theorem :: BVFUNC11:63 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) ) A1: ( 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) & Ex (('not' (Ex (a,A,G))),B,G) = Ex ((All (('not' a),A,G)),B,G) ) by Th19, BVFUNC_2:19; assume G is independent ; ::_thesis: Ex (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) hence Ex (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) by A1, Th45; ::_thesis: verum end; theorem :: BVFUNC11:64 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19; hence All (('not' (Ex (a,A,G))),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) by Th46; ::_thesis: verum end; theorem :: BVFUNC11:65 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) ) A1: ( 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) & Ex (('not' (Ex (a,A,G))),B,G) = Ex ((All (('not' a),A,G)),B,G) ) by Th19, BVFUNC_2:19; assume G is independent ; ::_thesis: Ex (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) hence Ex (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) by A1, Th47; ::_thesis: verum end; theorem :: BVFUNC11:66 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) ) A1: 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19; assume G is independent ; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) hence All (('not' (Ex (a,A,G))),B,G) '<' All ((Ex (('not' a),B,G)),A,G) by A1, Th48; ::_thesis: verum end; theorem :: BVFUNC11:67 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex ((All (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex ((All (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex ((All (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All (('not' (Ex (a,A,G))),B,G) '<' Ex ((All (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: All (('not' (Ex (a,A,G))),B,G) '<' Ex ((All (('not' a),B,G)),A,G) 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19; hence All (('not' (Ex (a,A,G))),B,G) '<' Ex ((All (('not' a),B,G)),A,G) by Th49; ::_thesis: verum end; theorem :: BVFUNC11:68 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),B,G)),A,G) ) A1: 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) by BVFUNC_2:19; assume G is independent ; ::_thesis: All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),B,G)),A,G) hence All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),B,G)),A,G) by A1, Th50; ::_thesis: verum end; theorem :: BVFUNC11:69 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) ) A1: 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) by Th19; assume G is independent ; ::_thesis: Ex ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) hence Ex ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) by A1, PARTIT_2:11, PARTIT_2:17; ::_thesis: verum end; theorem :: BVFUNC11:70 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) ) A1: ( 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) & All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) ) by BVFUNC_2:19; assume G is independent ; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) hence All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((All (a,B,G)),A,G)) by A1, Th33; ::_thesis: verum end; theorem :: BVFUNC11:71 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) ( 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) & All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) ) by BVFUNC_2:19; hence All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((Ex (a,B,G)),A,G)) by Th34; ::_thesis: verum end; theorem :: BVFUNC11:72 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((Ex (a,B,G)),A,G)) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((Ex (a,B,G)),A,G)) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((Ex (a,B,G)),A,G)) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((Ex (a,B,G)),A,G)) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((Ex (a,B,G)),A,G)) ) A1: ( 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) & All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) ) by BVFUNC_2:19; assume G is independent ; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((Ex (a,B,G)),A,G)) hence All ((All (('not' a),A,G)),B,G) '<' 'not' (Ex ((Ex (a,B,G)),A,G)) by A1, PARTIT_2:16; ::_thesis: verum end; theorem :: BVFUNC11:73 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) ) A1: 'not' (All ((All (a,A,G)),B,G)) = Ex ((Ex (('not' a),A,G)),B,G) by Th21; assume G is independent ; ::_thesis: Ex ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) hence Ex ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by A1, Th15; ::_thesis: verum end; theorem :: BVFUNC11:74 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) ) A1: 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G) by Th20; assume G is independent ; ::_thesis: All ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) hence All ((Ex (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by A1, Th38; ::_thesis: verum end; theorem :: BVFUNC11:75 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) ) A1: 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) by Th19; assume G is independent ; ::_thesis: Ex ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) hence Ex ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by A1, Th39; ::_thesis: verum end; theorem :: BVFUNC11:76 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) ( 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) & All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) ) by BVFUNC_2:19; hence All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (All (a,B,G))),A,G) by Th40; ::_thesis: verum end; theorem :: BVFUNC11:77 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) ) A1: 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) by Th19; assume G is independent ; ::_thesis: Ex ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) hence Ex ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) by A1, Th41; ::_thesis: verum end; theorem :: BVFUNC11:78 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) ) A1: ( 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) & All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) ) by BVFUNC_2:19; assume G is independent ; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) hence All ((All (('not' a),A,G)),B,G) '<' All (('not' (All (a,B,G))),A,G) by A1, Th42; ::_thesis: verum end; theorem :: BVFUNC11:79 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) ( 'not' (Ex ((Ex (a,A,G)),B,G)) = All (('not' (Ex (a,A,G))),B,G) & All (('not' (Ex (a,A,G))),B,G) = All ((All (('not' a),A,G)),B,G) ) by BVFUNC_2:19; hence All ((All (('not' a),A,G)),B,G) '<' Ex (('not' (Ex (a,B,G))),A,G) by Th43; ::_thesis: verum end; theorem :: BVFUNC11:80 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) = All (('not' (Ex (a,B,G))),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) = All (('not' (Ex (a,B,G))),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) = All (('not' (Ex (a,B,G))),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds All ((All (('not' a),A,G)),B,G) = All (('not' (Ex (a,B,G))),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies All ((All (('not' a),A,G)),B,G) = All (('not' (Ex (a,B,G))),A,G) ) assume G is independent ; ::_thesis: All ((All (('not' a),A,G)),B,G) = All (('not' (Ex (a,B,G))),A,G) then All ((All (('not' a),A,G)),B,G) = All ((All (('not' a),B,G)),A,G) by PARTIT_2:15; hence All ((All (('not' a),A,G)),B,G) = All (('not' (Ex (a,B,G))),A,G) by BVFUNC_2:19; ::_thesis: verum end; theorem :: BVFUNC11:81 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((Ex (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((Ex (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y holds All ((Ex (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y holds All ((Ex (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: All ((Ex (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) 'not' (Ex ((All (a,A,G)),B,G)) = All ((Ex (('not' a),A,G)),B,G) by Th20; hence All ((Ex (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) by Th13; ::_thesis: verum end; theorem :: BVFUNC11:82 for Y being non empty set for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) proof let Y be non empty set ; ::_thesis: for a being Function of Y,BOOLEAN for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let a be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y) for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let G be Subset of (PARTITIONS Y); ::_thesis: for A, B being a_partition of Y st G is independent holds Ex ((All (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) let A, B be a_partition of Y; ::_thesis: ( G is independent implies Ex ((All (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) ) A1: 'not' (All ((Ex (a,A,G)),B,G)) = Ex ((All (('not' a),A,G)),B,G) by Th19; assume G is independent ; ::_thesis: Ex ((All (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) hence Ex ((All (('not' a),A,G)),B,G) '<' Ex ((Ex (('not' a),B,G)),A,G) by A1, Th45; ::_thesis: verum end;