bvfunc11.miz



    begin

    reserve Y for non empty set,

a,b for Function of Y, BOOLEAN ,

G for Subset of ( PARTITIONS Y),

A,B for a_partition of Y;

    theorem :: BVFUNC11:1

    

     Th1: for z be Element of Y, PA,PB be a_partition of Y st PA '<' PB holds ( EqClass (z,PA)) c= ( EqClass (z,PB))

    proof

      let z be Element of Y;

      let PA,PB be a_partition of Y;

      assume PA '<' PB;

      then

       A1: ex b be 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 thesis by A1, EQREL_1:def 6;

    end;

    theorem :: BVFUNC11:2

    for z be Element of Y, PA,PB be a_partition of Y holds ( EqClass (z,PA)) c= ( EqClass (z,(PA '\/' PB))) by Th1, PARTIT1: 16;

    theorem :: BVFUNC11:3

    for z be Element of Y, PA,PB be a_partition of Y holds ( EqClass (z,(PA '/\' PB))) c= ( EqClass (z,PA)) by Th1, PARTIT1: 15;

    theorem :: BVFUNC11:4

    for z be Element of Y, PA be 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 G be Subset of ( PARTITIONS Y), A,B be a_partition of Y st G is independent & G = {A, B} & A <> B holds for a,b be set st a in A & b in B holds a meets b

    proof

      let G be Subset of ( PARTITIONS Y);

      let A,B be a_partition of Y;

      assume that

       A1: G is independent and

       A2: G = {A, B} and

       A3: A <> B;

      let a,b be set;

      assume that

       A4: a in A and

       A5: b in B;

      set h2 = ((A,B) --> (a,b));

      

       A6: for d be set st d in G holds (h2 . d) in d

      proof

        let d be set;

        assume d in G;

        then d = A or d = B by A2, TARSKI:def 2;

        hence thesis by A3, A4, A5, FUNCT_4: 63;

      end;

       {a, b} c= ( bool Y)

      proof

        let x be object;

        assume x in {a, b};

        then x = a or x = b by TARSKI:def 2;

        hence thesis by A4, A5;

      end;

      then

      reconsider SS = {a, b} as Subset-Family of Y;

      

       A7: ( dom h2) = {A, B} by FUNCT_4: 62;

      ( rng h2) = 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;

    end;

    theorem :: BVFUNC11:6

    for G be Subset of ( PARTITIONS Y), A,B be a_partition of Y st G is independent & G = {A, B} & A <> B holds ( '/\' G) = (A '/\' B)

    proof

      let G be Subset of ( PARTITIONS Y);

      let A,B be a_partition of Y;

      assume that

       A1: G is independent and

       A2: G = {A, B} and

       A3: A <> B;

      

       A4: ( '/\' G) c= (A '/\' B)

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in ( '/\' G);

        then

        consider h be Function, F be Subset-Family of Y such that

         A5: ( dom h) = G and

         A6: ( rng h) = F and

         A7: for d be 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= xx

        proof

          

           A15: ( rng h) = {(h . A), (h . B)}

          proof

            thus ( rng h) c= {(h . A), (h . B)}

            proof

              let m be object;

              assume m in ( rng h);

              then

              consider w be object 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 thesis by A17, TARSKI:def 2;

            end;

            let m be object;

            assume m in {(h . A), (h . B)};

            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 thesis by A18, A19, FUNCT_1:def 3;

          end;

          let m be object;

          assume

           A20: m in ((h . A) /\ (h . B));

          then

           A21: m in (h . B) by XBOOLE_0:def 4;

          m in (h . A) by A20, XBOOLE_0:def 4;

          then for y be set holds y in ( rng h) implies m in y by A21, A15, TARSKI:def 2;

          hence thesis by A8, A12, A13, SETFAM_1:def 1;

        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;

        xx c= ((h . A) /\ (h . B))

        proof

          let m be object;

          assume

           A25: m in xx;

          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 thesis by A26, XBOOLE_0:def 4;

        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 thesis by PARTIT1:def 4;

      end;

      (A '/\' B) c= ( '/\' G)

      proof

        let x be object;

        assume x in (A '/\' B);

        then x in (( INTERSECTION (A,B)) \ { {} }) by PARTIT1:def 4;

        then

        consider X,Z be 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 object;

          assume m in {X, Z};

          then m = X or m = Z by TARSKI:def 2;

          hence thesis by A28, A29;

        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 be set st d in G holds (h . d) in d

        proof

          let d be set;

          assume d in G;

          then d = A or d = B by A2, TARSKI:def 2;

          hence thesis by A3, A28, A29, FUNCT_4: 63;

        end;

        

         A33: ( dom h) = {A, B} by FUNCT_4: 62;

        

         A34: ( rng h) = SS by A3, FUNCT_4: 64;

        then ( Intersect SS) <> {} by A1, A2, A33, A32, BVFUNC_2:def 5;

        hence thesis by A2, A30, A33, A34, A32, A31, BVFUNC_2:def 1;

      end;

      hence thesis by A4;

    end;

    theorem :: BVFUNC11:7

    for G be Subset of ( PARTITIONS Y), A,B be a_partition of Y st G = {A, B} & A <> B holds ( CompF (A,G)) = B

    proof

      let G be Subset of ( PARTITIONS Y);

      let A,B be a_partition of Y;

      assume that

       A1: G = {A, B} and

       A2: A <> B;

      

       A3: ( '/\' {B}) c= B

      proof

        let x be object;

        assume x in ( '/\' {B});

        then

        consider h be Function, F be Subset-Family of Y such that

         A4: ( dom h) = {B} and

         A5: ( rng h) = F and

         A6: for d be 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 thesis by A8, SETFAM_1: 10;

      end;

      

       A9: B c= ( '/\' {B})

      proof

        let x be object;

        set h0 = (B .--> x);

        

         A10: ( dom h0) = {B};

        assume

         A11: x in B;

        

         A12: for d be set st d in {B} holds (h0 . d) in d

        proof

          let d be set;

          assume d in {B};

          then d = B by TARSKI:def 1;

          hence thesis by A11, FUNCOP_1: 72;

        end;

        

         A13: ( rng h0) = {x} by FUNCOP_1: 8;

        

         A14: x is set by TARSKI: 1;

        ( rng h0) c= ( bool Y)

        proof

          let m be object;

          assume m in ( rng h0);

          then m = x by A13, TARSKI:def 1;

          hence thesis by A11;

        end;

        then

        reconsider F0 = ( rng h0) as Subset-Family of Y;

        ( meet F0) = ( Intersect F0) by A13, SETFAM_1:def 9;

        then

         A15: x = ( Intersect F0) by A13, SETFAM_1: 10, A14;

        x <> {} by A11, EQREL_1:def 4;

        hence thesis by A10, A12, A15, BVFUNC_2:def 1;

      end;

      A in {A} by TARSKI:def 1;

      then

       A16: ( {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 A16, BVFUNC_2:def 7;

      hence thesis by A3, A9;

    end;

    begin

    theorem :: BVFUNC11:8

    

     Th8: a '<' b implies ( All (a,A,G)) '<' ( Ex (b,A,G))

    proof

      assume a '<' b;

      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 thesis by A1, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC11:9

    

     Th9: G is independent implies ( All (( All (a,A,G)),B,G)) '<' ( Ex (( All (a,B,G)),A,G))

    proof

      assume G is independent;

      then ( All (( All (a,A,G)),B,G)) = ( All (( All (a,B,G)),A,G)) by PARTIT_2: 15;

      hence thesis by Th8;

    end;

    theorem :: BVFUNC11:10

    ( All (( All (a,A,G)),B,G)) '<' ( Ex (( Ex (a,B,G)),A,G))

    proof

      

       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 thesis by A1, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC11:11

    G is independent implies ( All (( All (a,A,G)),B,G)) '<' ( All (( Ex (a,B,G)),A,G))

    proof

      assume G is independent;

      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 thesis by A1, PARTIT_2: 12;

    end;

    theorem :: BVFUNC11:12

    ( All (( Ex (a,A,G)),B,G)) '<' ( Ex (( Ex (a,B,G)),A,G))

    proof

      

       A1: ( Ex (a,B,G)) = ( B_SUP (a,( CompF (B,G)))) by BVFUNC_2:def 10;

      let z be Element of Y;

      assume

       A2: (( All (( Ex (a,A,G)),B,G)) . z) = TRUE ;

       A3:

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (B,G)))) holds (( Ex (a,A,G)) . x) = TRUE );

        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;

      end;

      

       A4: z in ( EqClass (z,( CompF (B,G)))) by EQREL_1:def 6;

      now

        assume not (ex x be Element of Y st x in ( EqClass (z,( CompF (A,G)))) & (a . x) = TRUE );

        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;

      end;

      then

      consider x1 be 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 thesis by BVFUNC_2:def 10;

    end;

    theorem :: BVFUNC11:13

    

     Th13: ( 'not' ( Ex (( All (a,A,G)),B,G))) '<' ( Ex (( Ex (( 'not' a),B,G)),A,G))

    proof

      

       A1: ( All (a,A,G)) = ( B_INF (a,( CompF (A,G)))) by BVFUNC_2:def 9;

      let z be Element of Y;

      

       A2: z in ( EqClass (z,( CompF (B,G)))) by EQREL_1:def 6;

      assume (( 'not' ( Ex (( All (a,A,G)),B,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 be 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 thesis by BVFUNC_2:def 10;

    end;

    theorem :: BVFUNC11:14

    

     Th14: G is independent implies ( Ex (( 'not' ( All (a,A,G))),B,G)) '<' ( Ex (( Ex (( 'not' a),B,G)),A,G))

    proof

      assume G is independent;

      then ( Ex (( Ex (( 'not' a),B,G)),A,G)) = ( Ex (( Ex (( 'not' a),A,G)),B,G)) by PARTIT_2: 16;

      hence thesis by BVFUNC_2: 18;

    end;

    theorem :: BVFUNC11:15

    

     Th15: G is independent implies ( 'not' ( All (( All (a,A,G)),B,G))) = ( Ex (( 'not' ( All (a,B,G))),A,G))

    proof

      assume G is independent;

      then ( All (( All (a,A,G)),B,G)) = ( All (( All (a,B,G)),A,G)) by PARTIT_2: 15;

      hence thesis by BVFUNC_2: 18;

    end;

    theorem :: BVFUNC11:16

    G is independent implies ( All (( 'not' ( All (a,A,G))),B,G)) '<' ( Ex (( Ex (( 'not' a),B,G)),A,G))

    proof

      assume G is independent;

      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 thesis by A1, Th8;

    end;

    theorem :: BVFUNC11:17

    G is independent implies ( 'not' ( All (( All (a,A,G)),B,G))) = ( Ex (( Ex (( 'not' a),B,G)),A,G))

    proof

      

       A1: ( Ex (( 'not' a),B,G)) = ( 'not' ( All (a,B,G))) by BVFUNC_2: 18;

      assume G is independent;

      hence thesis by A1, Th15;

    end;

    theorem :: BVFUNC11:18

    G is independent implies ( 'not' ( All (( All (a,A,G)),B,G))) '<' ( Ex (( Ex (( 'not' a),A,G)),B,G))

    proof

      assume

       A1: G is independent;

      then ( Ex (( 'not' ( All (a,B,G))),A,G)) '<' ( Ex (( Ex (( 'not' a),A,G)),B,G)) by Th14;

      hence thesis by A1, Th15;

    end;

    theorem :: BVFUNC11:19

    

     Th19: ( 'not' ( All (( Ex (a,A,G)),B,G))) = ( Ex (( All (( 'not' a),A,G)),B,G))

    proof

      ( 'not' ( All (( Ex (a,A,G)),B,G))) = ( Ex (( 'not' ( Ex (a,A,G))),B,G)) by BVFUNC_2: 18;

      hence thesis by BVFUNC_2: 19;

    end;

    theorem :: BVFUNC11:20

    

     Th20: ( 'not' ( Ex (( All (a,A,G)),B,G))) = ( All (( Ex (( 'not' a),A,G)),B,G))

    proof

      ( 'not' ( Ex (( All (a,A,G)),B,G))) = ( All (( 'not' ( All (a,A,G))),B,G)) by BVFUNC_2: 19;

      hence thesis by BVFUNC_2: 18;

    end;

    theorem :: BVFUNC11:21

    

     Th21: ( 'not' ( All (( All (a,A,G)),B,G))) = ( Ex (( Ex (( 'not' a),A,G)),B,G))

    proof

      ( Ex (( 'not' ( All (a,A,G))),B,G)) = ( Ex (( Ex (( 'not' a),A,G)),B,G)) by BVFUNC_2: 18;

      hence thesis by BVFUNC_2: 18;

    end;

    theorem :: BVFUNC11:22

    G is independent implies ( Ex (( All (a,A,G)),B,G)) '<' ( Ex (( Ex (a,B,G)),A,G))

    proof

      assume G is independent;

      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 thesis by A1, PARTIT_2: 13;

    end;

    theorem :: BVFUNC11:23

    ( All (( All (a,A,G)),B,G)) '<' ( All (( Ex (a,A,G)),B,G))

    proof

      ( All (a,A,G)) '<' ( Ex (a,A,G)) by Th8;

      hence thesis by PARTIT_2: 12;

    end;

    theorem :: BVFUNC11:24

    ( All (( All (a,A,G)),B,G)) '<' ( Ex (( Ex (a,A,G)),B,G))

    proof

      ( All (a,A,G)) '<' ( Ex (a,A,G)) by Th8;

      hence thesis by Th8;

    end;

    theorem :: BVFUNC11:25

    ( Ex (( All (a,A,G)),B,G)) '<' ( Ex (( Ex (a,A,G)),B,G))

    proof

      ( All (a,A,G)) '<' ( Ex (a,A,G)) by Th8;

      hence thesis by PARTIT_2: 13;

    end;

    theorem :: BVFUNC11:26

    

     Th26: G is independent implies ( All (( 'not' ( All (a,A,G))),B,G)) '<' ( 'not' ( All (( All (a,B,G)),A,G)))

    proof

      assume G is independent;

      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 thesis by PARTIT_2: 11;

    end;

    theorem :: BVFUNC11:27

    

     Th27: ( All (( All (( 'not' a),A,G)),B,G)) '<' ( 'not' ( All (( All (a,B,G)),A,G)))

    proof

      let z be Element of Y;

      

       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 ;

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (B,G)))) holds (( All (( 'not' a),A,G)) . x) = TRUE );

        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;

      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 thesis by MARGREL1:def 19;

    end;

    theorem :: BVFUNC11:28

    

     Th28: ( All (( 'not' ( Ex (a,A,G))),B,G)) '<' ( 'not' ( All (( All (a,B,G)),A,G)))

    proof

      ( All (( 'not' ( Ex (a,A,G))),B,G)) = ( All (( All (( 'not' a),A,G)),B,G)) by BVFUNC_2: 19;

      hence thesis by Th27;

    end;

    theorem :: BVFUNC11:29

    

     Th29: G is independent implies ( All (( Ex (( 'not' a),A,G)),B,G)) '<' ( 'not' ( All (( All (a,B,G)),A,G)))

    proof

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

      hence thesis by A1, Th9, PARTIT_2: 11;

    end;

    theorem :: BVFUNC11:30

    G is independent implies ( Ex (( All (( 'not' a),A,G)),B,G)) '<' ( 'not' ( All (( All (a,B,G)),A,G)))

    proof

      assume

       A1: G is independent;

      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 thesis by A1, PARTIT_2: 15;

    end;

    theorem :: BVFUNC11:31

    

     Th31: G is independent implies ( Ex (( 'not' ( Ex (a,A,G))),B,G)) '<' ( 'not' ( All (( All (a,B,G)),A,G)))

    proof

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

      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 thesis by A1, PARTIT_2: 11;

    end;

    theorem :: BVFUNC11:32

    G is independent implies ( 'not' ( All (( Ex (a,A,G)),B,G))) '<' ( 'not' ( Ex (( All (a,B,G)),A,G))) by PARTIT_2: 11, PARTIT_2: 17;

    theorem :: BVFUNC11:33

    

     Th33: G is independent implies ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( 'not' ( Ex (( All (a,B,G)),A,G)))

    proof

      assume G is independent;

      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 thesis by PARTIT_2: 11;

    end;

    theorem :: BVFUNC11:34

    

     Th34: ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( 'not' ( All (( Ex (a,B,G)),A,G)))

    proof

      let z be Element of Y;

      assume (( 'not' ( Ex (( Ex (a,A,G)),B,G))) . z) = TRUE ;

      then

       A1: ( 'not' (( Ex (( Ex (a,A,G)),B,G)) . z)) = TRUE by MARGREL1:def 19;

       A2:

      now

        assume ex x be Element of Y st x in ( EqClass (z,( CompF (B,G)))) & (( Ex (a,A,G)) . x) = TRUE ;

        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;

      end;

      

       A3: ( Ex (a,A,G)) = ( B_SUP (a,( CompF (A,G)))) by BVFUNC_2:def 10;

      

       A4: for x be Element of Y st x in ( EqClass (z,( CompF (B,G)))) holds for y be Element of Y st y in ( EqClass (x,( CompF (A,G)))) holds (a . y) <> TRUE

      proof

        let x be Element of Y;

        assume x in ( EqClass (z,( CompF (B,G))));

        then (( Ex (a,A,G)) . x) <> TRUE by A2;

        hence thesis by A3, BVFUNC_1:def 17;

      end;

      for x be Element of Y st x in ( EqClass (z,( CompF (B,G)))) holds (a . x) <> TRUE

      proof

        let x be Element of Y;

        

         A5: x in ( EqClass (x,( CompF (A,G)))) by EQREL_1:def 6;

        assume x in ( EqClass (z,( CompF (B,G))));

        hence thesis by A4, A5;

      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 thesis by MARGREL1:def 19;

    end;

    theorem :: BVFUNC11:35

    G is independent implies ( 'not' ( Ex (( All (a,A,G)),B,G))) '<' ( 'not' ( All (( All (a,B,G)),A,G)))

    proof

      assume G is independent;

      then ( All (( 'not' ( All (a,A,G))),B,G)) '<' ( 'not' ( All (( All (a,B,G)),A,G))) by Th26;

      hence thesis by BVFUNC_2: 19;

    end;

    theorem :: BVFUNC11:36

    G is independent implies ( 'not' ( All (( Ex (a,A,G)),B,G))) '<' ( 'not' ( All (( All (a,B,G)),A,G)))

    proof

      assume G is independent;

      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 thesis by A1, Th19;

    end;

    theorem :: BVFUNC11:37

    ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( 'not' ( All (( All (a,B,G)),A,G)))

    proof

      ( All (( 'not' ( Ex (a,A,G))),B,G)) '<' ( 'not' ( All (( All (a,B,G)),A,G))) by Th28;

      hence thesis by BVFUNC_2: 19;

    end;

    theorem :: BVFUNC11:38

    

     Th38: G is independent implies ( 'not' ( Ex (( All (a,A,G)),B,G))) '<' ( Ex (( 'not' ( All (a,B,G))),A,G))

    proof

      assume G is independent;

      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 thesis by A1, BVFUNC_2: 18;

    end;

    theorem :: BVFUNC11:39

    

     Th39: G is independent implies ( 'not' ( All (( Ex (a,A,G)),B,G))) '<' ( Ex (( 'not' ( All (a,B,G))),A,G))

    proof

      assume G is independent;

      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 thesis by A1, BVFUNC_2: 18;

    end;

    theorem :: BVFUNC11:40

    

     Th40: ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( Ex (( 'not' ( All (a,B,G))),A,G))

    proof

      ( 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 thesis by BVFUNC_2: 18;

    end;

    theorem :: BVFUNC11:41

    

     Th41: G is independent implies ( 'not' ( All (( Ex (a,A,G)),B,G))) '<' ( All (( 'not' ( All (a,B,G))),A,G))

    proof

      assume G is independent;

      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 thesis by BVFUNC_2: 19;

    end;

    theorem :: BVFUNC11:42

    

     Th42: G is independent implies ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( All (( 'not' ( All (a,B,G))),A,G))

    proof

      assume G is independent;

      then ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( 'not' ( Ex (( All (a,B,G)),A,G))) by Th33;

      hence thesis by BVFUNC_2: 19;

    end;

    theorem :: BVFUNC11:43

    

     Th43: ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( Ex (( 'not' ( Ex (a,B,G))),A,G))

    proof

      ( '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 thesis by Th19;

    end;

    theorem :: BVFUNC11:44

    

     Th44: G is independent implies ( 'not' ( Ex (( Ex (a,A,G)),B,G))) = ( All (( 'not' ( Ex (a,B,G))),A,G))

    proof

      assume G is independent;

      then ( 'not' ( Ex (( Ex (a,A,G)),B,G))) = ( 'not' ( Ex (( Ex (a,B,G)),A,G))) by PARTIT_2: 16;

      hence thesis by BVFUNC_2: 19;

    end;

    theorem :: BVFUNC11:45

    

     Th45: G is independent implies ( 'not' ( All (( Ex (a,A,G)),B,G))) '<' ( Ex (( Ex (( 'not' a),B,G)),A,G))

    proof

      assume G is independent;

      then ( 'not' ( All (( Ex (a,A,G)),B,G))) '<' ( Ex (( 'not' ( All (a,B,G))),A,G)) by Th39;

      hence thesis by BVFUNC_2: 18;

    end;

    theorem :: BVFUNC11:46

    

     Th46: ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( Ex (( Ex (( 'not' a),B,G)),A,G))

    proof

      ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( Ex (( 'not' ( All (a,B,G))),A,G)) by Th40;

      hence thesis by BVFUNC_2: 18;

    end;

    theorem :: BVFUNC11:47

    

     Th47: G is independent implies ( 'not' ( All (( Ex (a,A,G)),B,G))) '<' ( All (( Ex (( 'not' a),B,G)),A,G))

    proof

      assume G is independent;

      then ( 'not' ( All (( Ex (a,A,G)),B,G))) '<' ( All (( 'not' ( All (a,B,G))),A,G)) by Th41;

      hence thesis by BVFUNC_2: 18;

    end;

    theorem :: BVFUNC11:48

    

     Th48: G is independent implies ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( All (( Ex (( 'not' a),B,G)),A,G))

    proof

      assume G is independent;

      then ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( All (( 'not' ( All (a,B,G))),A,G)) by Th42;

      hence thesis by BVFUNC_2: 18;

    end;

    theorem :: BVFUNC11:49

    

     Th49: ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( Ex (( All (( 'not' a),B,G)),A,G))

    proof

      ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( Ex (( 'not' ( Ex (a,B,G))),A,G)) by Th43;

      hence thesis by BVFUNC_2: 19;

    end;

    theorem :: BVFUNC11:50

    

     Th50: G is independent implies ( 'not' ( Ex (( Ex (a,A,G)),B,G))) = ( All (( All (( 'not' a),B,G)),A,G))

    proof

      assume G is independent;

      then ( 'not' ( Ex (( Ex (a,A,G)),B,G))) = ( All (( 'not' ( Ex (a,B,G))),A,G)) by Th44;

      hence thesis by BVFUNC_2: 19;

    end;

    theorem :: BVFUNC11:51

    G is independent implies ( Ex (( 'not' ( Ex (a,A,G))),B,G)) '<' ( 'not' ( Ex (( All (a,B,G)),A,G)))

    proof

      assume G is independent;

      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 thesis by A1, BVFUNC_2: 19;

    end;

    theorem :: BVFUNC11:52

    ( All (( 'not' ( Ex (a,A,G))),B,G)) '<' ( 'not' ( Ex (( All (a,B,G)),A,G)))

    proof

      let z be Element of Y;

      

       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 ;

      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 be 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;

        assume x in ( EqClass (z,( CompF (A,G))));

        then

         A4: (a . x) <> TRUE by A2, BVFUNC_1:def 17;

        x in ( EqClass (x,( CompF (B,G)))) by EQREL_1:def 6;

        hence thesis by A3, A4, BVFUNC_1:def 16;

      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 thesis by MARGREL1:def 19;

    end;

    theorem :: BVFUNC11:53

    ( All (( 'not' ( Ex (a,A,G))),B,G)) '<' ( 'not' ( All (( Ex (a,B,G)),A,G)))

    proof

      ( 'not' ( Ex (( Ex (a,A,G)),B,G))) = ( All (( 'not' ( Ex (a,A,G))),B,G)) by BVFUNC_2: 19;

      hence thesis by Th34;

    end;

    theorem :: BVFUNC11:54

    G is independent implies ( All (( 'not' ( Ex (a,A,G))),B,G)) = ( 'not' ( Ex (( Ex (a,B,G)),A,G)))

    proof

      

       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;

      hence thesis by A1, PARTIT_2: 16;

    end;

    theorem :: BVFUNC11:55

    G is independent implies ( Ex (( 'not' ( All (a,A,G))),B,G)) = ( Ex (( 'not' ( All (a,B,G))),A,G))

    proof

      

       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;

      hence thesis by A1, Th15;

    end;

    theorem :: BVFUNC11:56

    G is independent implies ( All (( 'not' ( All (a,A,G))),B,G)) '<' ( Ex (( 'not' ( All (a,B,G))),A,G))

    proof

      

       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;

      hence thesis by A1, Th38;

    end;

    theorem :: BVFUNC11:57

    G is independent implies ( Ex (( 'not' ( Ex (a,A,G))),B,G)) '<' ( Ex (( 'not' ( All (a,B,G))),A,G))

    proof

      

       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;

      hence thesis by A1, Th39;

    end;

    theorem :: BVFUNC11:58

    ( All (( 'not' ( Ex (a,A,G))),B,G)) '<' ( Ex (( 'not' ( All (a,B,G))),A,G))

    proof

      ( 'not' ( Ex (( Ex (a,A,G)),B,G))) = ( All (( 'not' ( Ex (a,A,G))),B,G)) by BVFUNC_2: 19;

      hence thesis by Th40;

    end;

    theorem :: BVFUNC11:59

    G is independent implies ( Ex (( 'not' ( Ex (a,A,G))),B,G)) '<' ( All (( 'not' ( All (a,B,G))),A,G))

    proof

      

       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;

      hence thesis by A1, Th41;

    end;

    theorem :: BVFUNC11:60

    G is independent implies ( All (( 'not' ( Ex (a,A,G))),B,G)) '<' ( All (( 'not' ( All (a,B,G))),A,G))

    proof

      assume G is independent;

      then ( 'not' ( Ex (( Ex (a,A,G)),B,G))) '<' ( All (( 'not' ( All (a,B,G))),A,G)) by Th42;

      hence thesis by BVFUNC_2: 19;

    end;

    theorem :: BVFUNC11:61

    ( All (( 'not' ( Ex (a,A,G))),B,G)) '<' ( Ex (( 'not' ( Ex (a,B,G))),A,G))

    proof

      ( 'not' ( Ex (( Ex (a,A,G)),B,G))) = ( All (( 'not' ( Ex (a,A,G))),B,G)) by BVFUNC_2: 19;

      hence thesis by Th43;

    end;

    theorem :: BVFUNC11:62

    G is independent implies ( All (( 'not' ( Ex (a,A,G))),B,G)) = ( All (( 'not' ( Ex (a,B,G))),A,G))

    proof

      

       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;

      hence thesis by A1, Th44;

    end;

    theorem :: BVFUNC11:63

    G is independent implies ( Ex (( 'not' ( Ex (a,A,G))),B,G)) '<' ( Ex (( Ex (( 'not' a),B,G)),A,G))

    proof

      

       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;

      hence thesis by A1, Th45;

    end;

    theorem :: BVFUNC11:64

    ( All (( 'not' ( Ex (a,A,G))),B,G)) '<' ( Ex (( Ex (( 'not' a),B,G)),A,G))

    proof

      ( 'not' ( Ex (( Ex (a,A,G)),B,G))) = ( All (( 'not' ( Ex (a,A,G))),B,G)) by BVFUNC_2: 19;

      hence thesis by Th46;

    end;

    theorem :: BVFUNC11:65

    G is independent implies ( Ex (( 'not' ( Ex (a,A,G))),B,G)) '<' ( All (( Ex (( 'not' a),B,G)),A,G))

    proof

      

       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;

      hence thesis by A1, Th47;

    end;

    theorem :: BVFUNC11:66

    G is independent implies ( All (( 'not' ( Ex (a,A,G))),B,G)) '<' ( All (( Ex (( 'not' a),B,G)),A,G))

    proof

      

       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;

      hence thesis by A1, Th48;

    end;

    theorem :: BVFUNC11:67

    ( All (( 'not' ( Ex (a,A,G))),B,G)) '<' ( Ex (( All (( 'not' a),B,G)),A,G))

    proof

      ( 'not' ( Ex (( Ex (a,A,G)),B,G))) = ( All (( 'not' ( Ex (a,A,G))),B,G)) by BVFUNC_2: 19;

      hence thesis by Th49;

    end;

    theorem :: BVFUNC11:68

    G is independent implies ( All (( 'not' ( Ex (a,A,G))),B,G)) = ( All (( All (( 'not' a),B,G)),A,G))

    proof

      

       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;

      hence thesis by A1, Th50;

    end;

    theorem :: BVFUNC11:69

    G is independent implies ( Ex (( All (( 'not' a),A,G)),B,G)) '<' ( 'not' ( Ex (( All (a,B,G)),A,G)))

    proof

      

       A1: ( 'not' ( All (( Ex (a,A,G)),B,G))) = ( Ex (( All (( 'not' a),A,G)),B,G)) by Th19;

      assume G is independent;

      hence thesis by A1, PARTIT_2: 11, PARTIT_2: 17;

    end;

    theorem :: BVFUNC11:70

    G is independent implies ( All (( All (( 'not' a),A,G)),B,G)) '<' ( 'not' ( Ex (( All (a,B,G)),A,G)))

    proof

      

       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;

      hence thesis by A1, Th33;

    end;

    theorem :: BVFUNC11:71

    ( All (( All (( 'not' a),A,G)),B,G)) '<' ( 'not' ( All (( Ex (a,B,G)),A,G)))

    proof

      ( '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 thesis by Th34;

    end;

    theorem :: BVFUNC11:72

    G is independent implies ( All (( All (( 'not' a),A,G)),B,G)) '<' ( 'not' ( Ex (( Ex (a,B,G)),A,G)))

    proof

      

       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;

      hence thesis by A1, PARTIT_2: 16;

    end;

    theorem :: BVFUNC11:73

    G is independent implies ( Ex (( Ex (( 'not' a),A,G)),B,G)) '<' ( Ex (( 'not' ( All (a,B,G))),A,G))

    proof

      

       A1: ( 'not' ( All (( All (a,A,G)),B,G))) = ( Ex (( Ex (( 'not' a),A,G)),B,G)) by Th21;

      assume G is independent;

      hence thesis by A1, Th15;

    end;

    theorem :: BVFUNC11:74

    G is independent implies ( All (( Ex (( 'not' a),A,G)),B,G)) '<' ( Ex (( 'not' ( All (a,B,G))),A,G))

    proof

      

       A1: ( 'not' ( Ex (( All (a,A,G)),B,G))) = ( All (( Ex (( 'not' a),A,G)),B,G)) by Th20;

      assume G is independent;

      hence thesis by A1, Th38;

    end;

    theorem :: BVFUNC11:75

    G is independent implies ( Ex (( All (( 'not' a),A,G)),B,G)) '<' ( Ex (( 'not' ( All (a,B,G))),A,G))

    proof

      

       A1: ( 'not' ( All (( Ex (a,A,G)),B,G))) = ( Ex (( All (( 'not' a),A,G)),B,G)) by Th19;

      assume G is independent;

      hence thesis by A1, Th39;

    end;

    theorem :: BVFUNC11:76

    ( All (( All (( 'not' a),A,G)),B,G)) '<' ( Ex (( 'not' ( All (a,B,G))),A,G))

    proof

      ( '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 thesis by Th40;

    end;

    theorem :: BVFUNC11:77

    G is independent implies ( Ex (( All (( 'not' a),A,G)),B,G)) '<' ( All (( 'not' ( All (a,B,G))),A,G))

    proof

      

       A1: ( 'not' ( All (( Ex (a,A,G)),B,G))) = ( Ex (( All (( 'not' a),A,G)),B,G)) by Th19;

      assume G is independent;

      hence thesis by A1, Th41;

    end;

    theorem :: BVFUNC11:78

    G is independent implies ( All (( All (( 'not' a),A,G)),B,G)) '<' ( All (( 'not' ( All (a,B,G))),A,G))

    proof

      

       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;

      hence thesis by A1, Th42;

    end;

    theorem :: BVFUNC11:79

    ( All (( All (( 'not' a),A,G)),B,G)) '<' ( Ex (( 'not' ( Ex (a,B,G))),A,G))

    proof

      ( '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 thesis by Th43;

    end;

    theorem :: BVFUNC11:80

    G is independent implies ( All (( All (( 'not' a),A,G)),B,G)) = ( All (( 'not' ( Ex (a,B,G))),A,G))

    proof

      assume G is independent;

      then ( All (( All (( 'not' a),A,G)),B,G)) = ( All (( All (( 'not' a),B,G)),A,G)) by PARTIT_2: 15;

      hence thesis by BVFUNC_2: 19;

    end;

    theorem :: BVFUNC11:81

    ( All (( Ex (( 'not' a),A,G)),B,G)) '<' ( Ex (( Ex (( 'not' a),B,G)),A,G))

    proof

      ( 'not' ( Ex (( All (a,A,G)),B,G))) = ( All (( Ex (( 'not' a),A,G)),B,G)) by Th20;

      hence thesis by Th13;

    end;

    theorem :: BVFUNC11:82

    G is independent implies ( Ex (( All (( 'not' a),A,G)),B,G)) '<' ( Ex (( Ex (( 'not' a),B,G)),A,G))

    proof

      

       A1: ( 'not' ( All (( Ex (a,A,G)),B,G))) = ( Ex (( All (( 'not' a),A,G)),B,G)) by Th19;

      assume G is independent;

      hence thesis by A1, Th45;

    end;