bvfunc_3.miz



    begin

    reserve Y for non empty set,

G for Subset of ( PARTITIONS Y),

a,b,c,u for Function of Y, BOOLEAN ,

PA for a_partition of Y;

    theorem :: BVFUNC_3:1

    (a 'imp' b) '<' (( All (a,PA,G)) 'imp' ( Ex (b,PA,G)))

    proof

      let z be Element of Y;

      

       A1: ( 'not' (a . z)) = TRUE or ( 'not' (a . z)) = FALSE by XBOOLEAN:def 3;

      

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

      assume ((a 'imp' b) . z) = TRUE ;

      then

       A3: (( 'not' (a . z)) 'or' (b . z)) = TRUE by BVFUNC_1:def 8;

      per cases by A3, A1, BINARITH: 3;

        suppose ( 'not' (a . z)) = TRUE ;

        then (a . z) = FALSE by MARGREL1: 11;

        then (( B_INF (a,( CompF (PA,G)))) . z) = FALSE by A2, BVFUNC_1:def 16;

        then (( All (a,PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        

        hence ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' FALSE ) 'or' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 8

        .= ( TRUE 'or' (( Ex (b,PA,G)) . z)) by MARGREL1: 11

        .= TRUE by BINARITH: 10;

      end;

        suppose (b . z) = TRUE ;

        then (( B_SUP (b,( CompF (PA,G)))) . z) = TRUE by A2, BVFUNC_1:def 17;

        then (( Ex (b,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

        hence ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' (( All (a,PA,G)) . z)) 'or' TRUE ) by BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:2

    (( All (a,PA,G)) '&' ( All (b,PA,G))) '<' (a '&' b)

    proof

      let z be Element of Y;

      

       A1: ((( All (a,PA,G)) '&' ( All (b,PA,G))) . z) = ((( All (a,PA,G)) . z) '&' (( All (b,PA,G)) . z)) by MARGREL1:def 20;

      assume

       A2: ((( All (a,PA,G)) '&' ( All (b,PA,G))) . z) = TRUE ;

       A3:

      now

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

        then (( B_INF (a,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All (a,PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A2, A1, MARGREL1: 12;

      end;

      

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

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE );

        then (( B_INF (b,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All (b,PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A2, A1, MARGREL1: 12;

      end;

      then

       A5: (b . z) = TRUE by A4;

      

      thus ((a '&' b) . z) = ((a . z) '&' (b . z)) by MARGREL1:def 20

      .= ( TRUE '&' TRUE ) by A4, A3, A5

      .= TRUE ;

    end;

    theorem :: BVFUNC_3:3

    (a '&' b) '<' (( Ex (a,PA,G)) '&' ( Ex (b,PA,G)))

    proof

      let z be Element of Y;

      

       A1: ((a '&' b) . z) = ((a . z) '&' (b . z)) by MARGREL1:def 20;

      assume

       A2: ((a '&' b) . z) = TRUE ;

      then

       A3: ( Ex (a,PA,G)) = ( B_SUP (a,( CompF (PA,G)))) & (a . z) = TRUE by A1, BVFUNC_2:def 10, MARGREL1: 12;

      

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

      (b . z) = TRUE by A2, A1, MARGREL1: 12;

      then (( B_SUP (b,( CompF (PA,G)))) . z) = TRUE by A4, BVFUNC_1:def 17;

      then

       A5: (( Ex (b,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

      

      thus ((( Ex (a,PA,G)) '&' ( Ex (b,PA,G))) . z) = ((( Ex (a,PA,G)) . z) '&' (( Ex (b,PA,G)) . z)) by MARGREL1:def 20

      .= ( TRUE '&' TRUE ) by A3, A4, A5, BVFUNC_1:def 17

      .= TRUE ;

    end;

    theorem :: BVFUNC_3:4

    ( 'not' (( All (a,PA,G)) '&' ( All (b,PA,G)))) = (( Ex (( 'not' a),PA,G)) 'or' ( Ex (( 'not' b),PA,G)))

    proof

      

       A1: ( All (b,PA,G)) = ( B_INF (b,( CompF (PA,G)))) by BVFUNC_2:def 9;

      

       A2: ( All (a,PA,G)) = ( B_INF (a,( CompF (PA,G)))) by BVFUNC_2:def 9;

      

       A3: (( Ex (( 'not' a),PA,G)) 'or' ( Ex (( 'not' b),PA,G))) '<' ( 'not' (( All (a,PA,G)) '&' ( All (b,PA,G))))

      proof

        let z be Element of Y;

        

         A4: ((( Ex (( 'not' a),PA,G)) 'or' ( Ex (( 'not' b),PA,G))) . z) = ((( Ex (( 'not' a),PA,G)) . z) 'or' (( Ex (( 'not' b),PA,G)) . z)) by BVFUNC_1:def 4;

        

         A5: (( Ex (( 'not' b),PA,G)) . z) = TRUE or (( Ex (( 'not' b),PA,G)) . z) = FALSE by XBOOLEAN:def 3;

        assume

         A6: ((( Ex (( 'not' a),PA,G)) 'or' ( Ex (( 'not' b),PA,G))) . z) = TRUE ;

        per cases by A6, A4, A5, BINARITH: 3;

          suppose

           A7: (( Ex (( 'not' a),PA,G)) . z) = TRUE ;

          now

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

            then (( B_SUP (( 'not' a),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

            hence contradiction by A7, BVFUNC_2:def 10;

          end;

          then

          consider x1 be Element of Y such that

           A8: x1 in ( EqClass (z,( CompF (PA,G)))) and

           A9: (( 'not' a) . x1) = TRUE ;

          ( 'not' (a . x1)) = TRUE by A9, MARGREL1:def 19;

          then

           A10: (a . x1) = FALSE by MARGREL1: 11;

          

          thus (( 'not' (( All (a,PA,G)) '&' ( All (b,PA,G)))) . z) = ( 'not' ((( All (a,PA,G)) '&' ( All (b,PA,G))) . z)) by MARGREL1:def 19

          .= ( 'not' ((( All (a,PA,G)) . z) '&' (( All (b,PA,G)) . z))) by MARGREL1:def 20

          .= ( 'not' ( FALSE '&' (( All (b,PA,G)) . z))) by A2, A8, A10, BVFUNC_1:def 16

          .= ( 'not' FALSE ) by MARGREL1: 12

          .= TRUE by MARGREL1: 11;

        end;

          suppose

           A11: (( Ex (( 'not' b),PA,G)) . z) = TRUE ;

          now

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

            then (( B_SUP (( 'not' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

            hence contradiction by A11, BVFUNC_2:def 10;

          end;

          then

          consider x1 be Element of Y such that

           A12: x1 in ( EqClass (z,( CompF (PA,G)))) and

           A13: (( 'not' b) . x1) = TRUE ;

          ( 'not' (b . x1)) = TRUE by A13, MARGREL1:def 19;

          then

           A14: (b . x1) = FALSE by MARGREL1: 11;

          

          thus (( 'not' (( All (a,PA,G)) '&' ( All (b,PA,G)))) . z) = ( 'not' ((( All (a,PA,G)) '&' ( All (b,PA,G))) . z)) by MARGREL1:def 19

          .= ( 'not' ((( All (a,PA,G)) . z) '&' (( All (b,PA,G)) . z))) by MARGREL1:def 20

          .= ( 'not' ((( All (a,PA,G)) . z) '&' FALSE )) by A1, A12, A14, BVFUNC_1:def 16

          .= ( 'not' FALSE ) by MARGREL1: 12

          .= TRUE by MARGREL1: 11;

        end;

      end;

      ( 'not' (( All (a,PA,G)) '&' ( All (b,PA,G)))) '<' (( Ex (( 'not' a),PA,G)) 'or' ( Ex (( 'not' b),PA,G)))

      proof

        let z be Element of Y;

        assume (( 'not' (( All (a,PA,G)) '&' ( All (b,PA,G)))) . z) = TRUE ;

        then

         A15: ( 'not' ((( All (a,PA,G)) '&' ( All (b,PA,G))) . z)) = TRUE by MARGREL1:def 19;

        ((( All (a,PA,G)) '&' ( All (b,PA,G))) . z) = ((( All (a,PA,G)) . z) '&' (( All (b,PA,G)) . z)) by MARGREL1:def 20;

        then

         A16: ((( All (a,PA,G)) . z) '&' (( All (b,PA,G)) . z)) = FALSE by A15, MARGREL1: 11;

        per cases by A16, MARGREL1: 12;

          suppose (( All (a,PA,G)) . z) = FALSE ;

          then

          consider x1 be Element of Y such that

           A17: x1 in ( EqClass (z,( CompF (PA,G)))) and

           A18: (a . x1) <> TRUE by A2, BVFUNC_1:def 16;

          (a . x1) = FALSE by A18, XBOOLEAN:def 3;

          then ( 'not' (a . x1)) = TRUE by MARGREL1: 11;

          then (( 'not' a) . x1) = TRUE by MARGREL1:def 19;

          then (( B_SUP (( 'not' a),( CompF (PA,G)))) . z) = TRUE by A17, BVFUNC_1:def 17;

          then (( Ex (( 'not' a),PA,G)) . z) = TRUE by BVFUNC_2:def 10;

          

          hence ((( Ex (( 'not' a),PA,G)) 'or' ( Ex (( 'not' b),PA,G))) . z) = ( TRUE 'or' (( Ex (( 'not' b),PA,G)) . z)) by BVFUNC_1:def 4

          .= TRUE by BINARITH: 10;

        end;

          suppose (( All (b,PA,G)) . z) = FALSE ;

          then

          consider x1 be Element of Y such that

           A19: x1 in ( EqClass (z,( CompF (PA,G)))) and

           A20: (b . x1) <> TRUE by A1, BVFUNC_1:def 16;

          (b . x1) = FALSE by A20, XBOOLEAN:def 3;

          then ( 'not' (b . x1)) = TRUE by MARGREL1: 11;

          then (( 'not' b) . x1) = TRUE by MARGREL1:def 19;

          then (( B_SUP (( 'not' b),( CompF (PA,G)))) . z) = TRUE by A19, BVFUNC_1:def 17;

          then (( Ex (( 'not' b),PA,G)) . z) = TRUE by BVFUNC_2:def 10;

          

          hence ((( Ex (( 'not' a),PA,G)) 'or' ( Ex (( 'not' b),PA,G))) . z) = ((( Ex (( 'not' a),PA,G)) . z) 'or' TRUE ) by BVFUNC_1:def 4

          .= TRUE by BINARITH: 10;

        end;

      end;

      hence thesis by A3, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC_3:5

    ( 'not' (( Ex (a,PA,G)) '&' ( Ex (b,PA,G)))) = (( All (( 'not' a),PA,G)) 'or' ( All (( 'not' b),PA,G)))

    proof

      

       A1: ( All (( 'not' b),PA,G)) = ( B_INF (( 'not' b),( CompF (PA,G)))) by BVFUNC_2:def 9;

      

       A2: ( Ex (b,PA,G)) = ( B_SUP (b,( CompF (PA,G)))) by BVFUNC_2:def 10;

      

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

      

       A4: (( All (( 'not' a),PA,G)) 'or' ( All (( 'not' b),PA,G))) '<' ( 'not' (( Ex (a,PA,G)) '&' ( Ex (b,PA,G))))

      proof

        let z be Element of Y;

        

         A5: (( All (( 'not' b),PA,G)) . z) = TRUE or (( All (( 'not' b),PA,G)) . z) = FALSE by XBOOLEAN:def 3;

        assume ((( All (( 'not' a),PA,G)) 'or' ( All (( 'not' b),PA,G))) . z) = TRUE ;

        then

         A6: ((( All (( 'not' a),PA,G)) . z) 'or' (( All (( 'not' b),PA,G)) . z)) = TRUE by BVFUNC_1:def 4;

        per cases by A6, A5, BINARITH: 3;

          suppose

           A7: (( All (( 'not' a),PA,G)) . z) = TRUE ;

           A8:

          now

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

            then (( B_INF (( 'not' a),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

            hence contradiction by A7, BVFUNC_2:def 9;

          end;

           A9:

          now

            let x be Element of Y;

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

            then (( 'not' a) . x) = TRUE by A8;

            then ( 'not' (a . x)) = TRUE by MARGREL1:def 19;

            hence (a . x) <> TRUE by MARGREL1: 11;

          end;

          

          thus (( 'not' (( Ex (a,PA,G)) '&' ( Ex (b,PA,G)))) . z) = ( 'not' ((( Ex (a,PA,G)) '&' ( Ex (b,PA,G))) . z)) by MARGREL1:def 19

          .= ( 'not' ((( Ex (a,PA,G)) . z) '&' (( Ex (b,PA,G)) . z))) by MARGREL1:def 20

          .= ( 'not' ( FALSE '&' (( Ex (b,PA,G)) . z))) by A3, A9, BVFUNC_1:def 17

          .= ( 'not' FALSE ) by MARGREL1: 12

          .= TRUE by MARGREL1: 11;

        end;

          suppose

           A10: (( All (( 'not' b),PA,G)) . z) = TRUE ;

           A11:

          now

            assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (( 'not' b) . x) = TRUE );

            then (( B_INF (( 'not' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

            hence contradiction by A10, BVFUNC_2:def 9;

          end;

           A12:

          now

            let x be Element of Y;

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

            then (( 'not' b) . x) = TRUE by A11;

            then ( 'not' (b . x)) = TRUE by MARGREL1:def 19;

            hence (b . x) <> TRUE by MARGREL1: 11;

          end;

          

          thus (( 'not' (( Ex (a,PA,G)) '&' ( Ex (b,PA,G)))) . z) = ( 'not' ((( Ex (a,PA,G)) '&' ( Ex (b,PA,G))) . z)) by MARGREL1:def 19

          .= ( 'not' ((( Ex (a,PA,G)) . z) '&' (( Ex (b,PA,G)) . z))) by MARGREL1:def 20

          .= ( 'not' ((( Ex (a,PA,G)) . z) '&' FALSE )) by A2, A12, BVFUNC_1:def 17

          .= ( 'not' FALSE ) by MARGREL1: 12

          .= TRUE by MARGREL1: 11;

        end;

      end;

      

       A13: ( All (( 'not' a),PA,G)) = ( B_INF (( 'not' a),( CompF (PA,G)))) by BVFUNC_2:def 9;

      ( 'not' (( Ex (a,PA,G)) '&' ( Ex (b,PA,G)))) '<' (( All (( 'not' a),PA,G)) 'or' ( All (( 'not' b),PA,G)))

      proof

        let z be Element of Y;

        assume (( 'not' (( Ex (a,PA,G)) '&' ( Ex (b,PA,G)))) . z) = TRUE ;

        then ( 'not' ((( Ex (a,PA,G)) '&' ( Ex (b,PA,G))) . z)) = TRUE by MARGREL1:def 19;

        then ((( Ex (a,PA,G)) '&' ( Ex (b,PA,G))) . z) = FALSE by MARGREL1: 11;

        then

         A14: ((( Ex (a,PA,G)) . z) '&' (( Ex (b,PA,G)) . z)) = FALSE by MARGREL1:def 20;

        per cases by A14, MARGREL1: 12;

          suppose

           A15: (( Ex (a,PA,G)) . z) = FALSE ;

           A16:

          now

            let x be Element of Y;

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

            then (a . x) <> TRUE by A3, A15, BVFUNC_1:def 17;

            then (a . x) = FALSE by XBOOLEAN:def 3;

            then ( 'not' (a . x)) = TRUE by MARGREL1: 11;

            hence (( 'not' a) . x) = TRUE by MARGREL1:def 19;

          end;

          

          thus ((( All (( 'not' a),PA,G)) 'or' ( All (( 'not' b),PA,G))) . z) = ((( All (( 'not' a),PA,G)) . z) 'or' (( All (( 'not' b),PA,G)) . z)) by BVFUNC_1:def 4

          .= ( TRUE 'or' (( All (( 'not' b),PA,G)) . z)) by A13, A16, BVFUNC_1:def 16

          .= TRUE by BINARITH: 10;

        end;

          suppose

           A17: (( Ex (b,PA,G)) . z) = FALSE ;

           A18:

          now

            let x be Element of Y;

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

            then (b . x) <> TRUE by A2, A17, BVFUNC_1:def 17;

            then (b . x) = FALSE by XBOOLEAN:def 3;

            then ( 'not' (b . x)) = TRUE by MARGREL1: 11;

            hence (( 'not' b) . x) = TRUE by MARGREL1:def 19;

          end;

          

          thus ((( All (( 'not' a),PA,G)) 'or' ( All (( 'not' b),PA,G))) . z) = ((( All (( 'not' a),PA,G)) . z) 'or' (( All (( 'not' b),PA,G)) . z)) by BVFUNC_1:def 4

          .= ((( All (( 'not' a),PA,G)) . z) 'or' TRUE ) by A1, A18, BVFUNC_1:def 16

          .= TRUE by BINARITH: 10;

        end;

      end;

      hence thesis by A4, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC_3:6

    (( All (a,PA,G)) 'or' ( All (b,PA,G))) '<' (a 'or' b)

    proof

      let z be Element of Y;

      

       A1: (( All (a,PA,G)) . z) = TRUE or (( All (a,PA,G)) . z) = FALSE by XBOOLEAN:def 3;

      

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

      assume ((( All (a,PA,G)) 'or' ( All (b,PA,G))) . z) = TRUE ;

      then

       A3: ((( All (a,PA,G)) . z) 'or' (( All (b,PA,G)) . z)) = TRUE by BVFUNC_1:def 4;

      per cases by A3, A1, BINARITH: 3;

        suppose

         A4: (( All (a,PA,G)) . z) = TRUE ;

         A5:

        now

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

          then (( B_INF (a,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

          hence contradiction by A4, BVFUNC_2:def 9;

        end;

        

        thus ((a 'or' b) . z) = ((a . z) 'or' (b . z)) by BVFUNC_1:def 4

        .= ( TRUE 'or' (b . z)) by A2, A5

        .= TRUE by BINARITH: 10;

      end;

        suppose

         A6: (( All (b,PA,G)) . z) = TRUE ;

         A7:

        now

          assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE );

          then (( B_INF (b,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

          hence contradiction by A6, BVFUNC_2:def 9;

        end;

        

        thus ((a 'or' b) . z) = ((a . z) 'or' (b . z)) by BVFUNC_1:def 4

        .= ((a . z) 'or' TRUE ) by A2, A7

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:7

    (a 'or' b) '<' (( Ex (a,PA,G)) 'or' ( Ex (b,PA,G)))

    proof

      

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

      let z be Element of Y;

      

       A2: ( Ex (b,PA,G)) = ( B_SUP (b,( CompF (PA,G)))) by BVFUNC_2:def 10;

      

       A3: z in ( EqClass (z,( CompF (PA,G)))) by EQREL_1:def 6;

      assume ((a 'or' b) . z) = TRUE ;

      then

       A4: ((a . z) 'or' (b . z)) = TRUE by BVFUNC_1:def 4;

      

       A5: (b . z) = TRUE or (b . z) = FALSE by XBOOLEAN:def 3;

      per cases by A4, A5, BINARITH: 3;

        suppose

         A6: (a . z) = TRUE ;

        

        thus ((( Ex (a,PA,G)) 'or' ( Ex (b,PA,G))) . z) = ((( Ex (a,PA,G)) . z) 'or' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 4

        .= ( TRUE 'or' (( Ex (b,PA,G)) . z)) by A1, A3, A6, BVFUNC_1:def 17

        .= TRUE by BINARITH: 10;

      end;

        suppose

         A7: (b . z) = TRUE ;

        

        thus ((( Ex (a,PA,G)) 'or' ( Ex (b,PA,G))) . z) = ((( Ex (a,PA,G)) . z) 'or' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 4

        .= ((( Ex (a,PA,G)) . z) 'or' TRUE ) by A2, A3, A7, BVFUNC_1:def 17

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:8

    (a 'xor' b) '<' (( 'not' (( Ex (( 'not' a),PA,G)) 'xor' ( Ex (b,PA,G)))) 'or' ( 'not' (( Ex (a,PA,G)) 'xor' ( Ex (( 'not' b),PA,G)))))

    proof

      

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

      let z be Element of Y;

      

       A2: ( Ex (( 'not' b),PA,G)) = ( B_SUP (( 'not' b),( CompF (PA,G)))) by BVFUNC_2:def 10;

      

       A3: ((a . z) '&' ( 'not' (b . z))) = TRUE or ((a . z) '&' ( 'not' (b . z))) = FALSE by XBOOLEAN:def 3;

      

       A4: ((a 'xor' b) . z) = ((a . z) 'xor' (b . z)) by BVFUNC_1:def 5

      .= ((( 'not' (a . z)) '&' (b . z)) 'or' ((a . z) '&' ( 'not' (b . z))));

      

       A5: z in ( EqClass (z,( CompF (PA,G)))) by EQREL_1:def 6;

      

       A6: ( FALSE '&' TRUE ) = FALSE by MARGREL1: 13;

      assume

       A7: ((a 'xor' b) . z) = TRUE ;

      per cases by A7, A4, A3, BINARITH: 3;

        suppose

         A8: (( 'not' (a . z)) '&' (b . z)) = TRUE ;

        then ( 'not' (a . z)) = TRUE by MARGREL1: 12;

        then (( 'not' a) . z) = TRUE by MARGREL1:def 19;

        then

         A9: (( B_SUP (( 'not' a),( CompF (PA,G)))) . z) = TRUE by A5, BVFUNC_1:def 17;

        

         A10: (( 'not' (( Ex (a,PA,G)) 'xor' ( Ex (( 'not' b),PA,G)))) . z) = ( 'not' ((( Ex (a,PA,G)) 'xor' ( Ex (( 'not' b),PA,G))) . z)) by MARGREL1:def 19;

        (b . z) = TRUE by A8, MARGREL1: 12;

        then (( B_SUP (b,( CompF (PA,G)))) . z) = TRUE by A5, BVFUNC_1:def 17;

        then

         A11: (( Ex (b,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

         A12: ((( Ex (( 'not' a),PA,G)) 'xor' ( Ex (b,PA,G))) . z) = ((( Ex (( 'not' a),PA,G)) . z) 'xor' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 5

        .= FALSE by A1, A6, A9, A11, MARGREL1: 11;

        

        thus ((( 'not' (( Ex (( 'not' a),PA,G)) 'xor' ( Ex (b,PA,G)))) 'or' ( 'not' (( Ex (a,PA,G)) 'xor' ( Ex (( 'not' b),PA,G))))) . z) = ((( 'not' (( Ex (( 'not' a),PA,G)) 'xor' ( Ex (b,PA,G)))) . z) 'or' (( 'not' (( Ex (a,PA,G)) 'xor' ( Ex (( 'not' b),PA,G)))) . z)) by BVFUNC_1:def 4

        .= (( 'not' FALSE ) 'or' ( 'not' ((( Ex (a,PA,G)) 'xor' ( Ex (( 'not' b),PA,G))) . z))) by A12, A10, MARGREL1:def 19

        .= ( TRUE 'or' ( 'not' ((( Ex (a,PA,G)) 'xor' ( Ex (( 'not' b),PA,G))) . z))) by MARGREL1: 11

        .= TRUE by BINARITH: 10;

      end;

        suppose

         A13: ((a . z) '&' ( 'not' (b . z))) = TRUE ;

        then (a . z) = TRUE by MARGREL1: 12;

        then (( B_SUP (a,( CompF (PA,G)))) . z) = TRUE by A5, BVFUNC_1:def 17;

        then

         A14: (( Ex (a,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

         A15: (( 'not' (( Ex (a,PA,G)) 'xor' ( Ex (( 'not' b),PA,G)))) . z) = ( 'not' ((( Ex (a,PA,G)) 'xor' ( Ex (( 'not' b),PA,G))) . z)) by MARGREL1:def 19;

        ( 'not' (b . z)) = TRUE by A13, MARGREL1: 12;

        then (( 'not' b) . z) = TRUE by MARGREL1:def 19;

        then

         A16: (( B_SUP (( 'not' b),( CompF (PA,G)))) . z) = TRUE by A5, BVFUNC_1:def 17;

        

         A17: ((( Ex (a,PA,G)) 'xor' ( Ex (( 'not' b),PA,G))) . z) = ((( Ex (a,PA,G)) . z) 'xor' (( Ex (( 'not' b),PA,G)) . z)) by BVFUNC_1:def 5

        .= FALSE by A2, A6, A16, A14, MARGREL1: 11;

        

        thus ((( 'not' (( Ex (( 'not' a),PA,G)) 'xor' ( Ex (b,PA,G)))) 'or' ( 'not' (( Ex (a,PA,G)) 'xor' ( Ex (( 'not' b),PA,G))))) . z) = ((( 'not' (( Ex (( 'not' a),PA,G)) 'xor' ( Ex (b,PA,G)))) . z) 'or' (( 'not' (( Ex (a,PA,G)) 'xor' ( Ex (( 'not' b),PA,G)))) . z)) by BVFUNC_1:def 4

        .= (( 'not' ((( Ex (( 'not' a),PA,G)) 'xor' ( Ex (b,PA,G))) . z)) 'or' ( 'not' FALSE )) by A17, A15, MARGREL1:def 19

        .= (( 'not' ((( Ex (( 'not' a),PA,G)) 'xor' ( Ex (b,PA,G))) . z)) 'or' TRUE ) by MARGREL1: 11

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:9

    ( All ((a 'or' b),PA,G)) '<' (( All (a,PA,G)) 'or' ( Ex (b,PA,G)))

    proof

      let z be Element of Y;

      assume

       A1: (( All ((a 'or' b),PA,G)) . z) = TRUE ;

       A2:

      now

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

        then (( B_INF ((a 'or' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        hence contradiction by A1, BVFUNC_2:def 9;

      end;

      per cases ;

        suppose ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE ;

        then (( B_SUP (b,( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 17;

        then (( Ex (b,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

        hence ((( All (a,PA,G)) 'or' ( Ex (b,PA,G))) . z) = ((( All (a,PA,G)) . z) 'or' TRUE ) by BVFUNC_1:def 4

        .= TRUE by BINARITH: 10;

      end;

        suppose (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE ) & not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE );

        then (( B_INF (a,( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 16;

        then (( All (a,PA,G)) . z) = TRUE by BVFUNC_2:def 9;

        

        hence ((( All (a,PA,G)) 'or' ( Ex (b,PA,G))) . z) = ( TRUE 'or' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 4

        .= TRUE by BINARITH: 10;

      end;

        suppose

         A3: not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE ) & not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE );

        then

        consider x1 be Element of Y such that

         A4: x1 in ( EqClass (z,( CompF (PA,G)))) and

         A5: (a . x1) <> TRUE ;

        

         A6: (b . x1) <> TRUE by A3, A4;

        

         A7: (a . x1) = FALSE by A5, XBOOLEAN:def 3;

        ((a 'or' b) . x1) = ((a . x1) 'or' (b . x1)) by BVFUNC_1:def 4

        .= ( FALSE 'or' FALSE ) by A6, A7, XBOOLEAN:def 3

        .= FALSE ;

        hence thesis by A2, A4;

      end;

    end;

     Lm1:

    now

      let Y, a, b, G, PA;

      let z be Element of Y;

      assume

       A1: (( All ((a 'or' b),PA,G)) . z) = TRUE ;

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

      then (( B_INF ((a 'or' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

      hence contradiction by A1, BVFUNC_2:def 9;

    end;

    theorem :: BVFUNC_3:10

    ( All ((a 'or' b),PA,G)) '<' (( Ex (a,PA,G)) 'or' ( All (b,PA,G)))

    proof

      let z be Element of Y;

      assume

       A1: (( All ((a 'or' b),PA,G)) . z) = TRUE ;

      per cases ;

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

        then (( B_SUP (a,( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 17;

        then (( Ex (a,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

        hence ((( Ex (a,PA,G)) 'or' ( All (b,PA,G))) . z) = ( TRUE 'or' (( All (b,PA,G)) . z)) by BVFUNC_1:def 4

        .= TRUE by BINARITH: 10;

      end;

        suppose (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE ) & not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (a . x) = TRUE );

        then (( B_INF (b,( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 16;

        then (( All (b,PA,G)) . z) = TRUE by BVFUNC_2:def 9;

        

        hence ((( Ex (a,PA,G)) 'or' ( All (b,PA,G))) . z) = ((( Ex (a,PA,G)) . z) 'or' TRUE ) by BVFUNC_1:def 4

        .= TRUE by BINARITH: 10;

      end;

        suppose

         A2: not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE ) & not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (a . x) = TRUE );

        then

        consider x1 be Element of Y such that

         A3: x1 in ( EqClass (z,( CompF (PA,G)))) and

         A4: (b . x1) <> TRUE ;

        

         A5: (a . x1) <> TRUE by A2, A3;

        

         A6: (b . x1) = FALSE by A4, XBOOLEAN:def 3;

        ((a 'or' b) . x1) = ((a . x1) 'or' (b . x1)) by BVFUNC_1:def 4

        .= ( FALSE 'or' FALSE ) by A5, A6, XBOOLEAN:def 3

        .= FALSE ;

        hence thesis by A1, A3, Lm1;

      end;

    end;

    theorem :: BVFUNC_3:11

    ( All ((a 'or' b),PA,G)) '<' (( Ex (a,PA,G)) 'or' ( Ex (b,PA,G)))

    proof

      let z be Element of Y;

      

       A1: z in ( EqClass (z,( CompF (PA,G)))) by EQREL_1:def 6;

      assume (( All ((a 'or' b),PA,G)) . z) = TRUE ;

      then ((a 'or' b) . z) = TRUE by A1, Lm1;

      then

       A2: ((a . z) 'or' (b . z)) = TRUE by BVFUNC_1:def 4;

      

       A3: (a . z) = TRUE or (a . z) = FALSE by XBOOLEAN:def 3;

      per cases by A2, A3, BINARITH: 3;

        suppose (a . z) = TRUE ;

        then (( B_SUP (a,( CompF (PA,G)))) . z) = TRUE by A1, BVFUNC_1:def 17;

        then (( Ex (a,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

        hence ((( Ex (a,PA,G)) 'or' ( Ex (b,PA,G))) . z) = ( TRUE 'or' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 4

        .= TRUE by BINARITH: 10;

      end;

        suppose (b . z) = TRUE ;

        then (( B_SUP (b,( CompF (PA,G)))) . z) = TRUE by A1, BVFUNC_1:def 17;

        then (( Ex (b,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

        hence ((( Ex (a,PA,G)) 'or' ( Ex (b,PA,G))) . z) = ((( Ex (a,PA,G)) . z) 'or' TRUE ) by BVFUNC_1:def 4

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:12

    (( Ex (a,PA,G)) '&' ( All (b,PA,G))) '<' ( Ex ((a '&' b),PA,G))

    proof

      let z be Element of Y;

      assume ((( Ex (a,PA,G)) '&' ( All (b,PA,G))) . z) = TRUE ;

      then

       A1: ((( Ex (a,PA,G)) . z) '&' (( All (b,PA,G)) . z)) = TRUE by MARGREL1:def 20;

       A2:

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE );

        then (( B_INF (b,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All (b,PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

      now

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

        then (( B_SUP (a,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        then (( Ex (a,PA,G)) . z) = FALSE by BVFUNC_2:def 10;

        hence contradiction by A1, MARGREL1: 12;

      end;

      then

      consider x1 be Element of Y such that

       A3: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A4: (a . x1) = TRUE ;

      ((a '&' b) . x1) = ((a . x1) '&' (b . x1)) by MARGREL1:def 20

      .= ( TRUE '&' TRUE ) by A3, A4, A2

      .= TRUE ;

      then (( B_SUP ((a '&' b),( CompF (PA,G)))) . z) = TRUE by A3, BVFUNC_1:def 17;

      hence thesis by BVFUNC_2:def 10;

    end;

    theorem :: BVFUNC_3:13

    (( All (a,PA,G)) '&' ( Ex (b,PA,G))) '<' ( Ex ((a '&' b),PA,G))

    proof

      let z be Element of Y;

      assume ((( All (a,PA,G)) '&' ( Ex (b,PA,G))) . z) = TRUE ;

      then

       A1: ((( All (a,PA,G)) . z) '&' (( Ex (b,PA,G)) . z)) = TRUE by MARGREL1:def 20;

       A2:

      now

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

        then (( B_INF (a,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All (a,PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

      now

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

        then (( B_SUP (b,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        then (( Ex (b,PA,G)) . z) = FALSE by BVFUNC_2:def 10;

        hence contradiction by A1, MARGREL1: 12;

      end;

      then

      consider x1 be Element of Y such that

       A3: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A4: (b . x1) = TRUE ;

      ((a '&' b) . x1) = ((a . x1) '&' (b . x1)) by MARGREL1:def 20

      .= ( TRUE '&' TRUE ) by A3, A4, A2

      .= TRUE ;

      then (( B_SUP ((a '&' b),( CompF (PA,G)))) . z) = TRUE by A3, BVFUNC_1:def 17;

      hence thesis by BVFUNC_2:def 10;

    end;

     Lm2:

    now

      let Y, a, b, G, PA;

      let z be Element of Y;

      assume

       A1: (( All ((a 'imp' b),PA,G)) . z) = TRUE ;

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

      then (( B_INF ((a 'imp' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

      hence contradiction by A1, BVFUNC_2:def 9;

    end;

    theorem :: BVFUNC_3:14

    ( All ((a 'imp' b),PA,G)) '<' (( All (a,PA,G)) 'imp' ( Ex (b,PA,G)))

    proof

      

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

      let z be Element of Y;

      assume

       A2: (( All ((a 'imp' b),PA,G)) . z) = TRUE ;

      

       A3: z in ( EqClass (z,( CompF (PA,G)))) by EQREL_1:def 6;

      per cases ;

        suppose ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE ;

        then (( B_SUP (b,( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 17;

        then (( Ex (b,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

        hence ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' (( All (a,PA,G)) . z)) 'or' TRUE ) by BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

        suppose (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE ) & not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE );

        then

         A4: (b . z) <> TRUE & (a . z) = TRUE by A3;

        ((a 'imp' b) . z) = (( 'not' (a . z)) 'or' (b . z)) by BVFUNC_1:def 8

        .= (( 'not' TRUE ) 'or' FALSE ) by A4, XBOOLEAN:def 3

        .= ( FALSE 'or' FALSE ) by MARGREL1: 11

        .= FALSE ;

        hence thesis by A2, A3, Lm2;

      end;

        suppose

         A5: not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (a . x) = TRUE ) & not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE );

        

        thus ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' (( All (a,PA,G)) . z)) 'or' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 8

        .= (( 'not' FALSE ) 'or' (( Ex (b,PA,G)) . z)) by A1, A5, BVFUNC_1:def 16

        .= ( TRUE 'or' (( Ex (b,PA,G)) . z)) by MARGREL1: 11

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:15

    ( All ((a 'imp' b),PA,G)) '<' (( Ex (a,PA,G)) 'imp' ( Ex (b,PA,G)))

    proof

      

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

      let z be Element of Y;

      assume

       A2: (( All ((a 'imp' b),PA,G)) . z) = TRUE ;

      per cases ;

        suppose ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE ;

        then (( B_SUP (b,( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 17;

        then (( Ex (b,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

        hence ((( Ex (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' (( Ex (a,PA,G)) . z)) 'or' TRUE ) by BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

        suppose

         A3: (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (a . x) = TRUE ) & not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE );

        then

        consider x1 be Element of Y such that

         A4: x1 in ( EqClass (z,( CompF (PA,G)))) and

         A5: (a . x1) = TRUE ;

        

         A6: (b . x1) <> TRUE by A3, A4;

        ((a 'imp' b) . x1) = (( 'not' (a . x1)) 'or' (b . x1)) by BVFUNC_1:def 8

        .= (( 'not' TRUE ) 'or' FALSE ) by A5, A6, XBOOLEAN:def 3

        .= ( FALSE 'or' FALSE ) by MARGREL1: 11

        .= FALSE ;

        hence thesis by A2, A4, Lm2;

      end;

        suppose

         A7: not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (a . x) = TRUE ) & not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (b . x) = TRUE );

        

        thus ((( Ex (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' (( Ex (a,PA,G)) . z)) 'or' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 8

        .= (( 'not' FALSE ) 'or' (( Ex (b,PA,G)) . z)) by A1, A7, BVFUNC_1:def 17

        .= ( TRUE 'or' (( Ex (b,PA,G)) . z)) by MARGREL1: 11

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:16

    (( Ex (a,PA,G)) 'imp' ( All (b,PA,G))) '<' ( All ((a 'imp' b),PA,G))

    proof

      let z be Element of Y;

      assume ((( Ex (a,PA,G)) 'imp' ( All (b,PA,G))) . z) = TRUE ;

      then

       A1: (( 'not' (( Ex (a,PA,G)) . z)) 'or' (( All (b,PA,G)) . z)) = TRUE by BVFUNC_1:def 8;

      per cases ;

        suppose

         A2: for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE ;

        for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((a 'imp' b) . x) = TRUE

        proof

          let x be Element of Y;

          assume

           A3: x in ( EqClass (z,( CompF (PA,G))));

          

          thus ((a 'imp' b) . x) = (( 'not' (a . x)) 'or' (b . x)) by BVFUNC_1:def 8

          .= (( 'not' (a . x)) 'or' TRUE ) by A2, A3

          .= TRUE by BINARITH: 10;

        end;

        then (( B_INF ((a 'imp' b),( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 16;

        hence thesis by BVFUNC_2:def 9;

      end;

        suppose

         A4: (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (a . x) = TRUE ) & not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE );

        then (( B_SUP (a,( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 17;

        then (( Ex (a,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        then

         A5: ( 'not' (( Ex (a,PA,G)) . z)) = FALSE by MARGREL1: 11;

        (( B_INF (b,( CompF (PA,G)))) . z) = FALSE by A4, BVFUNC_1:def 16;

        then (( All (b,PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence thesis by A1, A5;

      end;

        suppose

         A6: not (ex x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) & (a . x) = TRUE ) & not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE );

        now

          let x be Element of Y;

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

          then

           A7: (a . x) <> TRUE by A6;

          

          thus ((a 'imp' b) . x) = (( 'not' (a . x)) 'or' (b . x)) by BVFUNC_1:def 8

          .= (( 'not' FALSE ) 'or' (b . x)) by A7, XBOOLEAN:def 3

          .= ( TRUE 'or' (b . x)) by MARGREL1: 11

          .= TRUE by BINARITH: 10;

        end;

        then (( B_INF ((a 'imp' b),( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 16;

        hence thesis by BVFUNC_2:def 9;

      end;

    end;

    theorem :: BVFUNC_3:17

    (a 'imp' b) '<' (a 'imp' ( Ex (b,PA,G)))

    proof

      let z be Element of Y;

      

       A1: ( 'not' (a . z)) = TRUE or ( 'not' (a . z)) = FALSE by XBOOLEAN:def 3;

      

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

      assume ((a 'imp' b) . z) = TRUE ;

      then

       A3: (( 'not' (a . z)) 'or' (b . z)) = TRUE by BVFUNC_1:def 8;

      per cases by A3, A1, BINARITH: 3;

        suppose ( 'not' (a . z)) = TRUE ;

        

        hence ((a 'imp' ( Ex (b,PA,G))) . z) = ( TRUE 'or' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

        suppose (b . z) = TRUE ;

        then (( B_SUP (b,( CompF (PA,G)))) . z) = TRUE by A2, BVFUNC_1:def 17;

        then (( Ex (b,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

        hence ((a 'imp' ( Ex (b,PA,G))) . z) = (( 'not' (a . z)) 'or' TRUE ) by BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:18

    (a 'imp' b) '<' (( All (a,PA,G)) 'imp' b)

    proof

      let z be Element of Y;

      

       A1: ( 'not' (a . z)) = TRUE or ( 'not' (a . z)) = FALSE by XBOOLEAN:def 3;

      

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

      assume ((a 'imp' b) . z) = TRUE ;

      then

       A3: (( 'not' (a . z)) 'or' (b . z)) = TRUE by BVFUNC_1:def 8;

      per cases by A3, A1, BINARITH: 3;

        suppose ( 'not' (a . z)) = TRUE ;

        then (a . z) = FALSE by MARGREL1: 11;

        then (( B_INF (a,( CompF (PA,G)))) . z) = FALSE by A2, BVFUNC_1:def 16;

        then (( All (a,PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        

        hence ((( All (a,PA,G)) 'imp' b) . z) = (( 'not' FALSE ) 'or' (b . z)) by BVFUNC_1:def 8

        .= ( TRUE 'or' (b . z)) by MARGREL1: 11

        .= TRUE by BINARITH: 10;

      end;

        suppose (b . z) = TRUE ;

        

        hence ((( All (a,PA,G)) 'imp' b) . z) = (( 'not' (( All (a,PA,G)) . z)) 'or' TRUE ) by BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:19

    ( Ex ((a 'imp' b),PA,G)) '<' (( All (a,PA,G)) 'imp' ( Ex (b,PA,G)))

    proof

      let z be Element of Y;

      assume

       A1: (( Ex ((a 'imp' b),PA,G)) . z) = TRUE ;

      now

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

        then (( B_SUP ((a 'imp' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        hence contradiction by A1, BVFUNC_2:def 10;

      end;

      then

      consider x1 be Element of Y such that

       A2: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A3: ((a 'imp' b) . x1) = TRUE ;

      

       A4: (( 'not' (a . x1)) 'or' (b . x1)) = TRUE by A3, BVFUNC_1:def 8;

      

       A5: (b . x1) = TRUE or (b . x1) = FALSE by XBOOLEAN:def 3;

      per cases by A4, A5, BINARITH: 3;

        suppose ( 'not' (a . x1)) = TRUE ;

        then (a . x1) = FALSE by MARGREL1: 11;

        then (( B_INF (a,( CompF (PA,G)))) . z) = FALSE by A2, BVFUNC_1:def 16;

        then (( All (a,PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        

        hence ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' FALSE ) 'or' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 8

        .= ( TRUE 'or' (( Ex (b,PA,G)) . z)) by MARGREL1: 11

        .= TRUE by BINARITH: 10;

      end;

        suppose (b . x1) = TRUE ;

        then (( B_SUP (b,( CompF (PA,G)))) . z) = TRUE by A2, BVFUNC_1:def 17;

        then (( Ex (b,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

        hence ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' (( All (a,PA,G)) . z)) 'or' TRUE ) by BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:20

    ( All (a,PA,G)) '<' (( Ex (b,PA,G)) 'imp' ( Ex ((a '&' b),PA,G)))

    proof

      let z be Element of Y;

      assume

       A1: (( All (a,PA,G)) . z) = TRUE ;

       A2:

      now

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

        then (( B_INF (a,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        hence contradiction by A1, BVFUNC_2:def 9;

      end;

      per cases ;

        suppose

         A3: (( Ex (b,PA,G)) . z) = TRUE ;

        now

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

          then (( B_SUP (b,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

          hence contradiction by A3, BVFUNC_2:def 10;

        end;

        then

        consider x1 be Element of Y such that

         A4: x1 in ( EqClass (z,( CompF (PA,G)))) and

         A5: (b . x1) = TRUE ;

        ((a '&' b) . x1) = ((a . x1) '&' (b . x1)) by MARGREL1:def 20

        .= ( TRUE '&' TRUE ) by A2, A4, A5

        .= TRUE ;

        then (( B_SUP ((a '&' b),( CompF (PA,G)))) . z) = TRUE by A4, BVFUNC_1:def 17;

        then (( Ex ((a '&' b),PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

        hence ((( Ex (b,PA,G)) 'imp' ( Ex ((a '&' b),PA,G))) . z) = (( 'not' (( Ex (b,PA,G)) . z)) 'or' TRUE ) by BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

        suppose (( Ex (b,PA,G)) . z) <> TRUE ;

        then (( Ex (b,PA,G)) . z) = FALSE by XBOOLEAN:def 3;

        

        hence ((( Ex (b,PA,G)) 'imp' ( Ex ((a '&' b),PA,G))) . z) = (( 'not' FALSE ) 'or' (( Ex ((a '&' b),PA,G)) . z)) by BVFUNC_1:def 8

        .= ( TRUE 'or' (( Ex ((a '&' b),PA,G)) . z)) by MARGREL1: 11

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:21

    u is_independent_of (PA,G) implies ( Ex ((u 'imp' a),PA,G)) '<' (u 'imp' ( Ex (a,PA,G)))

    proof

      assume u is_independent_of (PA,G);

      then

       A1: u is_dependent_of ( CompF (PA,G)) by BVFUNC_2:def 8;

      let z be Element of Y;

      

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

      assume

       A3: (( Ex ((u 'imp' a),PA,G)) . z) = TRUE ;

      now

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

        then (( B_SUP ((u 'imp' a),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        hence contradiction by A3, BVFUNC_2:def 10;

      end;

      then

      consider x1 be Element of Y such that

       A4: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A5: ((u 'imp' a) . x1) = TRUE ;

      

       A6: (( 'not' (u . x1)) 'or' (a . x1)) = TRUE by A5, BVFUNC_1:def 8;

      

       A7: ( 'not' (u . x1)) = TRUE or ( 'not' (u . x1)) = FALSE by XBOOLEAN:def 3;

      per cases by A6, A7, BINARITH: 3;

        suppose

         A8: ( 'not' (u . x1)) = TRUE ;

        (u . x1) = (u . z) by A1, A4, A2;

        then (u . z) = FALSE by A8, MARGREL1: 11;

        

        hence ((u 'imp' ( Ex (a,PA,G))) . z) = (( 'not' FALSE ) 'or' (( Ex (a,PA,G)) . z)) by BVFUNC_1:def 8

        .= ( TRUE 'or' (( Ex (a,PA,G)) . z)) by MARGREL1: 11

        .= TRUE by BINARITH: 10;

      end;

        suppose (a . x1) = TRUE ;

        then (( B_SUP (a,( CompF (PA,G)))) . z) = TRUE by A4, BVFUNC_1:def 17;

        then (( Ex (a,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

        hence ((u 'imp' ( Ex (a,PA,G))) . z) = (( 'not' (u . z)) 'or' TRUE ) by BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:22

    u is_independent_of (PA,G) implies ( Ex ((a 'imp' u),PA,G)) '<' (( All (a,PA,G)) 'imp' u)

    proof

      assume u is_independent_of (PA,G);

      then

       A1: u is_dependent_of ( CompF (PA,G)) by BVFUNC_2:def 8;

      let z be Element of Y;

      

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

      assume

       A3: (( Ex ((a 'imp' u),PA,G)) . z) = TRUE ;

      now

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

        then (( B_SUP ((a 'imp' u),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        hence contradiction by A3, BVFUNC_2:def 10;

      end;

      then

      consider x1 be Element of Y such that

       A4: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A5: ((a 'imp' u) . x1) = TRUE ;

      

       A6: (( 'not' (a . x1)) 'or' (u . x1)) = TRUE by A5, BVFUNC_1:def 8;

      

       A7: ( 'not' (a . x1)) = TRUE or ( 'not' (a . x1)) = FALSE by XBOOLEAN:def 3;

      per cases by A6, A7, BINARITH: 3;

        suppose ( 'not' (a . x1)) = TRUE ;

        then (a . x1) = FALSE by MARGREL1: 11;

        then (( B_INF (a,( CompF (PA,G)))) . z) = FALSE by A4, BVFUNC_1:def 16;

        then (( All (a,PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        

        hence ((( All (a,PA,G)) 'imp' u) . z) = (( 'not' FALSE ) 'or' (u . z)) by BVFUNC_1:def 8

        .= ( TRUE 'or' (u . z)) by MARGREL1: 11

        .= TRUE by BINARITH: 10;

      end;

        suppose

         A8: (u . x1) = TRUE ;

        (u . x1) = (u . z) by A1, A4, A2;

        

        hence ((( All (a,PA,G)) 'imp' u) . z) = (( 'not' (( All (a,PA,G)) . z)) 'or' TRUE ) by A8, BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:23

    (( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) = ( Ex ((a 'imp' b),PA,G))

    proof

      

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

      

       A2: (( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) '<' ( Ex ((a 'imp' b),PA,G))

      proof

        let z be Element of Y;

        

         A3: ( 'not' (( All (a,PA,G)) . z)) = TRUE or ( 'not' (( All (a,PA,G)) . z)) = FALSE by XBOOLEAN:def 3;

        assume ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = TRUE ;

        then

         A4: (( 'not' (( All (a,PA,G)) . z)) 'or' (( Ex (b,PA,G)) . z)) = TRUE by BVFUNC_1:def 8;

        per cases by A4, A3, BINARITH: 3;

          suppose ( 'not' (( All (a,PA,G)) . z)) = TRUE ;

          then (( All (a,PA,G)) . z) = FALSE by MARGREL1: 11;

          then

          consider x1 be Element of Y such that

           A5: x1 in ( EqClass (z,( CompF (PA,G)))) and

           A6: (a . x1) <> TRUE by A1, BVFUNC_1:def 16;

          ((a 'imp' b) . x1) = (( 'not' (a . x1)) 'or' (b . x1)) by BVFUNC_1:def 8

          .= (( 'not' FALSE ) 'or' (b . x1)) by A6, XBOOLEAN:def 3

          .= ( TRUE 'or' (b . x1)) by MARGREL1: 11

          .= TRUE by BINARITH: 10;

          then (( B_SUP ((a 'imp' b),( CompF (PA,G)))) . z) = TRUE by A5, BVFUNC_1:def 17;

          hence thesis by BVFUNC_2:def 10;

        end;

          suppose

           A7: (( Ex (b,PA,G)) . z) = TRUE ;

          now

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

            then (( B_SUP (b,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

            hence contradiction by A7, BVFUNC_2:def 10;

          end;

          then

          consider x1 be Element of Y such that

           A8: x1 in ( EqClass (z,( CompF (PA,G)))) and

           A9: (b . x1) = TRUE ;

          ((a 'imp' b) . x1) = (( 'not' (a . x1)) 'or' TRUE ) by A9, BVFUNC_1:def 8

          .= TRUE by BINARITH: 10;

          then (( B_SUP ((a 'imp' b),( CompF (PA,G)))) . z) = TRUE by A8, BVFUNC_1:def 17;

          hence thesis by BVFUNC_2:def 10;

        end;

      end;

      ( Ex ((a 'imp' b),PA,G)) '<' (( All (a,PA,G)) 'imp' ( Ex (b,PA,G)))

      proof

        let z be Element of Y;

        assume

         A10: (( Ex ((a 'imp' b),PA,G)) . z) = TRUE ;

        now

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

          then (( B_SUP ((a 'imp' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

          hence contradiction by A10, BVFUNC_2:def 10;

        end;

        then

        consider x1 be Element of Y such that

         A11: x1 in ( EqClass (z,( CompF (PA,G)))) and

         A12: ((a 'imp' b) . x1) = TRUE ;

        

         A13: (( 'not' (a . x1)) 'or' (b . x1)) = TRUE by A12, BVFUNC_1:def 8;

        

         A14: ( 'not' (a . x1)) = TRUE or ( 'not' (a . x1)) = FALSE by XBOOLEAN:def 3;

        per cases by A13, A14, BINARITH: 3;

          suppose ( 'not' (a . x1)) = TRUE ;

          then (a . x1) = FALSE by MARGREL1: 11;

          then (( B_INF (a,( CompF (PA,G)))) . z) = FALSE by A11, BVFUNC_1:def 16;

          

          hence ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' FALSE ) 'or' (( Ex (b,PA,G)) . z)) by A1, BVFUNC_1:def 8

          .= ( TRUE 'or' (( Ex (b,PA,G)) . z)) by MARGREL1: 11

          .= TRUE by BINARITH: 10;

        end;

          suppose (b . x1) = TRUE ;

          then (( B_SUP (b,( CompF (PA,G)))) . z) = TRUE by A11, BVFUNC_1:def 17;

          then (( Ex (b,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

          

          hence ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' (( All (a,PA,G)) . z)) 'or' TRUE ) by BVFUNC_1:def 8

          .= TRUE by BINARITH: 10;

        end;

      end;

      hence thesis by A2, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC_3:24

    (( All (a,PA,G)) 'imp' ( All (b,PA,G))) '<' (( All (a,PA,G)) 'imp' ( Ex (b,PA,G)))

    proof

      let z be Element of Y;

      

       A1: ( 'not' (( All (a,PA,G)) . z)) = TRUE or ( 'not' (( All (a,PA,G)) . z)) = FALSE by XBOOLEAN:def 3;

      

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

      assume ((( All (a,PA,G)) 'imp' ( All (b,PA,G))) . z) = TRUE ;

      then

       A3: (( 'not' (( All (a,PA,G)) . z)) 'or' (( All (b,PA,G)) . z)) = TRUE by BVFUNC_1:def 8;

      per cases by A3, A1, BINARITH: 3;

        suppose ( 'not' (( All (a,PA,G)) . z)) = TRUE ;

        

        hence ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = ( TRUE 'or' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

        suppose

         A4: (( All (b,PA,G)) . z) = TRUE ;

        now

          assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds (b . x) = TRUE );

          then (( B_INF (b,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

          hence contradiction by A4, BVFUNC_2:def 9;

        end;

        then (b . z) = TRUE by A2;

        then (( B_SUP (b,( CompF (PA,G)))) . z) = TRUE by A2, BVFUNC_1:def 17;

        then (( Ex (b,PA,G)) . z) = TRUE by BVFUNC_2:def 10;

        

        hence ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' (( All (a,PA,G)) . z)) 'or' TRUE ) by BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:25

    (( Ex (a,PA,G)) 'imp' ( Ex (b,PA,G))) '<' (( All (a,PA,G)) 'imp' ( Ex (b,PA,G)))

    proof

      

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

      let z be Element of Y;

      

       A2: ( 'not' (( Ex (a,PA,G)) . z)) = TRUE or ( 'not' (( Ex (a,PA,G)) . z)) = FALSE by XBOOLEAN:def 3;

      assume ((( Ex (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = TRUE ;

      then

       A3: (( 'not' (( Ex (a,PA,G)) . z)) 'or' (( Ex (b,PA,G)) . z)) = TRUE by BVFUNC_1:def 8;

      

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

      per cases by A3, A2, BINARITH: 3;

        suppose ( 'not' (( Ex (a,PA,G)) . z)) = TRUE ;

        then (( Ex (a,PA,G)) . z) = FALSE by MARGREL1: 11;

        then (a . z) <> TRUE by A1, A4, BVFUNC_1:def 17;

        then (( B_INF (a,( CompF (PA,G)))) . z) = FALSE by A4, BVFUNC_1:def 16;

        then (( All (a,PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        

        hence ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' FALSE ) 'or' (( Ex (b,PA,G)) . z)) by BVFUNC_1:def 8

        .= ( TRUE 'or' (( Ex (b,PA,G)) . z)) by MARGREL1: 11

        .= TRUE by BINARITH: 10;

      end;

        suppose (( Ex (b,PA,G)) . z) = TRUE ;

        

        hence ((( All (a,PA,G)) 'imp' ( Ex (b,PA,G))) . z) = (( 'not' (( All (a,PA,G)) . z)) 'or' TRUE ) by BVFUNC_1:def 8

        .= TRUE by BINARITH: 10;

      end;

    end;

    theorem :: BVFUNC_3:26

    

     Th26: ( All ((a 'imp' b),PA,G)) = ( All ((( 'not' a) 'or' b),PA,G))

    proof

      

       A1: ( All ((( 'not' a) 'or' b),PA,G)) '<' ( All ((a 'imp' b),PA,G))

      proof

        let z be Element of Y;

        assume

         A2: (( All ((( 'not' a) 'or' b),PA,G)) . z) = TRUE ;

         A3:

        now

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

          then (( B_INF ((( 'not' a) 'or' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

          hence contradiction by A2, BVFUNC_2:def 9;

        end;

        for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((a 'imp' b) . x) = TRUE

        proof

          let x be Element of Y;

          

           A4: (( 'not' a) . x) = TRUE or (( 'not' a) . x) = FALSE by XBOOLEAN:def 3;

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

          then ((( 'not' a) 'or' b) . x) = TRUE by A3;

          then

           A5: ((( 'not' a) . x) 'or' (b . x)) = TRUE by BVFUNC_1:def 4;

          per cases by A5, A4, BINARITH: 3;

            suppose (( 'not' a) . x) = TRUE ;

            then ( 'not' (a . x)) = TRUE by MARGREL1:def 19;

            

            hence ((a 'imp' b) . x) = ( TRUE 'or' (b . x)) by BVFUNC_1:def 8

            .= TRUE by BINARITH: 10;

          end;

            suppose (b . x) = TRUE ;

            

            hence ((a 'imp' b) . x) = (( 'not' (a . x)) 'or' TRUE ) by BVFUNC_1:def 8

            .= TRUE by BINARITH: 10;

          end;

        end;

        then (( B_INF ((a 'imp' b),( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 16;

        hence thesis by BVFUNC_2:def 9;

      end;

      ( All ((a 'imp' b),PA,G)) '<' ( All ((( 'not' a) 'or' b),PA,G))

      proof

        let z be Element of Y;

        assume

         A6: (( All ((a 'imp' b),PA,G)) . z) = TRUE ;

         A7:

        now

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

          then (( B_INF ((a 'imp' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

          hence contradiction by A6, BVFUNC_2:def 9;

        end;

        now

          let x be Element of Y;

          

           A8: ( 'not' (a . x)) = TRUE or ( 'not' (a . x)) = FALSE by XBOOLEAN:def 3;

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

          then ((a 'imp' b) . x) = TRUE by A7;

          then

           A9: (( 'not' (a . x)) 'or' (b . x)) = TRUE by BVFUNC_1:def 8;

          per cases by A9, A8, BINARITH: 3;

            suppose ( 'not' (a . x)) = TRUE ;

            then (( 'not' a) . x) = TRUE by MARGREL1:def 19;

            

            hence ((( 'not' a) 'or' b) . x) = ( TRUE 'or' (b . x)) by BVFUNC_1:def 4

            .= TRUE by BINARITH: 10;

          end;

            suppose (b . x) = TRUE ;

            

            hence ((( 'not' a) 'or' b) . x) = ((( 'not' a) . x) 'or' TRUE ) by BVFUNC_1:def 4

            .= TRUE by BINARITH: 10;

          end;

        end;

        then (( B_INF ((( 'not' a) 'or' b),( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 16;

        hence thesis by BVFUNC_2:def 9;

      end;

      hence thesis by A1, BVFUNC_1: 15;

    end;

    theorem :: BVFUNC_3:27

    ( All ((a 'imp' b),PA,G)) = ( 'not' ( Ex ((a '&' ( 'not' b)),PA,G)))

    proof

      ( 'not' ( All ((( 'not' a) 'or' b),PA,G))) = ( Ex (( 'not' (( 'not' a) 'or' b)),PA,G)) & ( 'not' (( 'not' a) 'or' b)) = (( 'not' ( 'not' a)) '&' ( 'not' b)) by BVFUNC_1: 13, BVFUNC_2: 18;

      hence thesis by Th26;

    end;

    theorem :: BVFUNC_3:28

    ( Ex (a,PA,G)) '<' ( 'not' (( All ((a 'imp' b),PA,G)) '&' ( All ((a 'imp' ( 'not' b)),PA,G))))

    proof

      let z be Element of Y;

      

       A1: (( 'not' (( All ((a 'imp' b),PA,G)) '&' ( All ((a 'imp' ( 'not' b)),PA,G)))) . z) = ( 'not' ((( All ((a 'imp' b),PA,G)) '&' ( All ((a 'imp' ( 'not' b)),PA,G))) . z)) by MARGREL1:def 19

      .= ( 'not' ((( All ((a 'imp' b),PA,G)) . z) '&' (( All ((a 'imp' ( 'not' b)),PA,G)) . z))) by MARGREL1:def 20;

      assume

       A2: (( Ex (a,PA,G)) . z) = TRUE ;

      now

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

        then (( B_SUP (a,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        hence contradiction by A2, BVFUNC_2:def 10;

      end;

      then

      consider x1 be Element of Y such that

       A3: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A4: (a . x1) = TRUE ;

      

       A5: ((a 'imp' b) . x1) = (( 'not' TRUE ) 'or' (b . x1)) by A4, BVFUNC_1:def 8

      .= ( FALSE 'or' (b . x1)) by MARGREL1: 11

      .= (b . x1) by BINARITH: 3;

      

       A6: ((a 'imp' ( 'not' b)) . x1) = (( 'not' TRUE ) 'or' (( 'not' b) . x1)) by A4, BVFUNC_1:def 8

      .= ( FALSE 'or' (( 'not' b) . x1)) by MARGREL1: 11

      .= (( 'not' b) . x1) by BINARITH: 3;

      per cases by XBOOLEAN:def 3;

        suppose (b . x1) = TRUE ;

        

        then ((a 'imp' ( 'not' b)) . x1) = ( 'not' TRUE ) by A6, MARGREL1:def 19

        .= FALSE by MARGREL1: 11;

        then (( B_INF ((a 'imp' ( 'not' b)),( CompF (PA,G)))) . z) = FALSE by A3, BVFUNC_1:def 16;

        

        hence (( 'not' (( All ((a 'imp' b),PA,G)) '&' ( All ((a 'imp' ( 'not' b)),PA,G)))) . z) = ( 'not' ((( All ((a 'imp' b),PA,G)) . z) '&' FALSE )) by A1, BVFUNC_2:def 9

        .= ( 'not' FALSE ) by MARGREL1: 12

        .= TRUE by MARGREL1: 11;

      end;

        suppose (b . x1) = FALSE ;

        then (( B_INF ((a 'imp' b),( CompF (PA,G)))) . z) = FALSE by A3, A5, BVFUNC_1:def 16;

        

        hence (( 'not' (( All ((a 'imp' b),PA,G)) '&' ( All ((a 'imp' ( 'not' b)),PA,G)))) . z) = ( 'not' ( FALSE '&' (( All ((a 'imp' ( 'not' b)),PA,G)) . z))) by A1, BVFUNC_2:def 9

        .= ( 'not' FALSE ) by MARGREL1: 12

        .= TRUE by MARGREL1: 11;

      end;

    end;

    theorem :: BVFUNC_3:29

    ( Ex (a,PA,G)) '<' ( 'not' (( 'not' ( Ex ((a '&' b),PA,G))) '&' ( 'not' ( Ex ((a '&' ( 'not' b)),PA,G)))))

    proof

      let z be Element of Y;

      

       A1: (( 'not' ( Ex ((a '&' ( 'not' b)),PA,G))) . z) = ( 'not' (( Ex ((a '&' ( 'not' b)),PA,G)) . z)) by MARGREL1:def 19;

      

       A2: (( 'not' (( 'not' ( Ex ((a '&' b),PA,G))) '&' ( 'not' ( Ex ((a '&' ( 'not' b)),PA,G))))) . z) = ( 'not' ((( 'not' ( Ex ((a '&' b),PA,G))) '&' ( 'not' ( Ex ((a '&' ( 'not' b)),PA,G)))) . z)) by MARGREL1:def 19

      .= ( 'not' ((( 'not' ( Ex ((a '&' b),PA,G))) . z) '&' (( 'not' ( Ex ((a '&' ( 'not' b)),PA,G))) . z))) by MARGREL1:def 20

      .= ( 'not' (( 'not' (( Ex ((a '&' b),PA,G)) . z)) '&' ( 'not' (( Ex ((a '&' ( 'not' b)),PA,G)) . z)))) by A1, MARGREL1:def 19;

      assume

       A3: (( Ex (a,PA,G)) . z) = TRUE ;

      now

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

        then (( B_SUP (a,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        hence contradiction by A3, BVFUNC_2:def 10;

      end;

      then

      consider x1 be Element of Y such that

       A4: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A5: (a . x1) = TRUE ;

      

       A6: ((a '&' b) . x1) = ( TRUE '&' (b . x1)) by A5, MARGREL1:def 20

      .= (b . x1) by MARGREL1: 14;

      

       A7: ((a '&' ( 'not' b)) . x1) = ( TRUE '&' (( 'not' b) . x1)) by A5, MARGREL1:def 20

      .= (( 'not' b) . x1) by MARGREL1: 14;

      per cases by XBOOLEAN:def 3;

        suppose (b . x1) = TRUE ;

        then (( B_SUP ((a '&' b),( CompF (PA,G)))) . z) = TRUE by A4, A6, BVFUNC_1:def 17;

        

        hence (( 'not' (( 'not' ( Ex ((a '&' b),PA,G))) '&' ( 'not' ( Ex ((a '&' ( 'not' b)),PA,G))))) . z) = ( 'not' (( 'not' TRUE ) '&' ( 'not' (( Ex ((a '&' ( 'not' b)),PA,G)) . z)))) by A2, BVFUNC_2:def 10

        .= ( 'not' ( FALSE '&' ( 'not' (( Ex ((a '&' ( 'not' b)),PA,G)) . z)))) by MARGREL1: 11

        .= ( 'not' FALSE ) by MARGREL1: 12

        .= TRUE by MARGREL1: 11;

      end;

        suppose (b . x1) = FALSE ;

        then ((a '&' ( 'not' b)) . x1) = ( 'not' FALSE ) by A7, MARGREL1:def 19;

        then ((a '&' ( 'not' b)) . x1) = TRUE by MARGREL1: 11;

        then (( B_SUP ((a '&' ( 'not' b)),( CompF (PA,G)))) . z) = TRUE by A4, BVFUNC_1:def 17;

        

        hence (( 'not' (( 'not' ( Ex ((a '&' b),PA,G))) '&' ( 'not' ( Ex ((a '&' ( 'not' b)),PA,G))))) . z) = ( 'not' (( 'not' (( Ex ((a '&' b),PA,G)) . z)) '&' ( 'not' TRUE ))) by A2, BVFUNC_2:def 10

        .= ( 'not' (( 'not' (( Ex ((a '&' b),PA,G)) . z)) '&' FALSE )) by MARGREL1: 11

        .= ( 'not' FALSE ) by MARGREL1: 12

        .= TRUE by MARGREL1: 11;

      end;

    end;

    theorem :: BVFUNC_3:30

    (( Ex (a,PA,G)) '&' ( All ((a 'imp' b),PA,G))) '<' ( Ex ((a '&' b),PA,G))

    proof

      let z be Element of Y;

      

       A1: ( 'not' FALSE ) = TRUE by MARGREL1: 11;

      assume ((( Ex (a,PA,G)) '&' ( All ((a 'imp' b),PA,G))) . z) = TRUE ;

      then

       A2: ((( Ex (a,PA,G)) . z) '&' (( All ((a 'imp' b),PA,G)) . z)) = TRUE by MARGREL1:def 20;

      now

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

        then (( B_SUP (a,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        then (( Ex (a,PA,G)) . z) = FALSE by BVFUNC_2:def 10;

        hence contradiction by A2, MARGREL1: 12;

      end;

      then

      consider x1 be Element of Y such that

       A3: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A4: (a . x1) = TRUE ;

      now

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

        then (( B_INF ((a 'imp' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((a 'imp' b),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A2, MARGREL1: 12;

      end;

      then ((a 'imp' b) . x1) = TRUE by A3;

      then

       A5: (( 'not' (a . x1)) 'or' (b . x1)) = TRUE by BVFUNC_1:def 8;

      ((a '&' b) . x1) = ((a . x1) '&' (b . x1)) by MARGREL1:def 20

      .= ( TRUE '&' TRUE ) by A4, A5, A1, BINARITH: 3

      .= TRUE ;

      then (( B_SUP ((a '&' b),( CompF (PA,G)))) . z) = TRUE by A3, BVFUNC_1:def 17;

      hence thesis by BVFUNC_2:def 10;

    end;

    theorem :: BVFUNC_3:31

    (( Ex (a,PA,G)) '&' ( 'not' ( Ex ((a '&' b),PA,G)))) '<' ( 'not' ( All ((a 'imp' b),PA,G)))

    proof

      let z be Element of Y;

      assume ((( Ex (a,PA,G)) '&' ( 'not' ( Ex ((a '&' b),PA,G)))) . z) = TRUE ;

      then

       A1: ((( Ex (a,PA,G)) . z) '&' (( 'not' ( Ex ((a '&' b),PA,G))) . z)) = TRUE by MARGREL1:def 20;

      now

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

        then (( B_SUP (a,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        then (( Ex (a,PA,G)) . z) = FALSE by BVFUNC_2:def 10;

        hence contradiction by A1, MARGREL1: 12;

      end;

      then

      consider x1 be Element of Y such that

       A2: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A3: (a . x1) = TRUE ;

      (( 'not' ( Ex ((a '&' b),PA,G))) . z) = TRUE by A1, MARGREL1: 12;

      then ( 'not' (( Ex ((a '&' b),PA,G)) . z)) = TRUE by MARGREL1:def 19;

      then ( Ex ((a '&' b),PA,G)) = ( B_SUP ((a '&' b),( CompF (PA,G)))) & (( Ex ((a '&' b),PA,G)) . z) = FALSE by BVFUNC_2:def 10, MARGREL1: 11;

      then ((a '&' b) . x1) <> TRUE by A2, BVFUNC_1:def 17;

      then ((a '&' b) . x1) = FALSE by XBOOLEAN:def 3;

      then

       A4: ((a . x1) '&' (b . x1)) = FALSE by MARGREL1:def 20;

      per cases by A4, MARGREL1: 12;

        suppose (a . x1) = FALSE ;

        hence thesis by A3;

      end;

        suppose (b . x1) = FALSE ;

        

        then ((a 'imp' b) . x1) = (( 'not' TRUE ) 'or' FALSE ) by A3, BVFUNC_1:def 8

        .= ( FALSE 'or' FALSE ) by MARGREL1: 11

        .= FALSE ;

        then (( B_INF ((a 'imp' b),( CompF (PA,G)))) . z) = FALSE by A2, BVFUNC_1:def 16;

        then (( All ((a 'imp' b),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        

        hence (( 'not' ( All ((a 'imp' b),PA,G))) . z) = ( 'not' FALSE ) by MARGREL1:def 19

        .= TRUE by MARGREL1: 11;

      end;

    end;

    theorem :: BVFUNC_3:32

    (( All ((a 'imp' c),PA,G)) '&' ( All ((c 'imp' b),PA,G))) '<' ( All ((a 'imp' b),PA,G))

    proof

      let z be Element of Y;

      assume ((( All ((a 'imp' c),PA,G)) '&' ( All ((c 'imp' b),PA,G))) . z) = TRUE ;

      then

       A1: ((( All ((a 'imp' c),PA,G)) . z) '&' (( All ((c 'imp' b),PA,G)) . z)) = TRUE by MARGREL1:def 20;

       A2:

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((c 'imp' b) . x) = TRUE );

        then (( B_INF ((c 'imp' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((c 'imp' b),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

       A3:

      now

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

        then (( B_INF ((a 'imp' c),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((a 'imp' c),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

      for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((a 'imp' b) . x) = TRUE

      proof

        let x be Element of Y;

        

         A4: ( 'not' (a . x)) = TRUE or ( 'not' (a . x)) = FALSE by XBOOLEAN:def 3;

        

         A5: ( 'not' (c . x)) = TRUE or ( 'not' (c . x)) = FALSE by XBOOLEAN:def 3;

        assume

         A6: x in ( EqClass (z,( CompF (PA,G))));

        then ((a 'imp' c) . x) = TRUE by A3;

        then

         A7: (( 'not' (a . x)) 'or' (c . x)) = TRUE by BVFUNC_1:def 8;

        ((c 'imp' b) . x) = TRUE by A2, A6;

        then

         A8: (( 'not' (c . x)) 'or' (b . x)) = TRUE by BVFUNC_1:def 8;

        per cases by A7, A4, A8, A5, BINARITH: 3;

          suppose ( 'not' (a . x)) = TRUE & ( 'not' (c . x)) = TRUE ;

          

          hence ((a 'imp' b) . x) = ( TRUE 'or' (b . x)) by BVFUNC_1:def 8

          .= TRUE by BINARITH: 10;

        end;

          suppose ( 'not' (a . x)) = TRUE & (b . x) = TRUE ;

          

          hence ((a 'imp' b) . x) = ( TRUE 'or' (b . x)) by BVFUNC_1:def 8

          .= TRUE by BINARITH: 10;

        end;

          suppose (c . x) = TRUE & ( 'not' (c . x)) = TRUE ;

          hence thesis by MARGREL1: 11;

        end;

          suppose (c . x) = TRUE & (b . x) = TRUE ;

          

          hence ((a 'imp' b) . x) = (( 'not' (a . x)) 'or' TRUE ) by BVFUNC_1:def 8

          .= TRUE by BINARITH: 10;

        end;

      end;

      then (( B_INF ((a 'imp' b),( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 16;

      hence thesis by BVFUNC_2:def 9;

    end;

    theorem :: BVFUNC_3:33

    (( All ((c 'imp' b),PA,G)) '&' ( Ex ((a '&' c),PA,G))) '<' ( Ex ((a '&' b),PA,G))

    proof

      let z be Element of Y;

      assume ((( All ((c 'imp' b),PA,G)) '&' ( Ex ((a '&' c),PA,G))) . z) = TRUE ;

      then

       A1: ((( All ((c 'imp' b),PA,G)) . z) '&' (( Ex ((a '&' c),PA,G)) . z)) = TRUE by MARGREL1:def 20;

      now

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

        then (( B_SUP ((a '&' c),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        then (( Ex ((a '&' c),PA,G)) . z) = FALSE by BVFUNC_2:def 10;

        hence contradiction by A1, MARGREL1: 12;

      end;

      then

      consider x1 be Element of Y such that

       A2: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A3: ((a '&' c) . x1) = TRUE ;

      

       A4: ((a . x1) '&' (c . x1)) = TRUE by A3, MARGREL1:def 20;

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((c 'imp' b) . x) = TRUE );

        then (( B_INF ((c 'imp' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((c 'imp' b),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

      then ((c 'imp' b) . x1) = TRUE by A2;

      then

       A5: (( 'not' (c . x1)) 'or' (b . x1)) = TRUE by BVFUNC_1:def 8;

      

       A6: ( 'not' (c . x1)) = TRUE or ( 'not' (c . x1)) = FALSE by XBOOLEAN:def 3;

      per cases by A5, A6, A4, BINARITH: 3, MARGREL1: 12;

        suppose (a . x1) = TRUE & (c . x1) = TRUE & ( 'not' (c . x1)) = TRUE ;

        hence thesis by MARGREL1: 11;

      end;

        suppose (a . x1) = TRUE & (c . x1) = TRUE & (b . x1) = TRUE ;

        

        then ((a '&' b) . x1) = ( TRUE '&' TRUE ) by MARGREL1:def 20

        .= TRUE ;

        then (( B_SUP ((a '&' b),( CompF (PA,G)))) . z) = TRUE by A2, BVFUNC_1:def 17;

        hence thesis by BVFUNC_2:def 10;

      end;

    end;

    theorem :: BVFUNC_3:34

    (( All ((b 'imp' ( 'not' c)),PA,G)) '&' ( All ((a 'imp' c),PA,G))) '<' ( All ((a 'imp' ( 'not' b)),PA,G))

    proof

      let z be Element of Y;

      assume ((( All ((b 'imp' ( 'not' c)),PA,G)) '&' ( All ((a 'imp' c),PA,G))) . z) = TRUE ;

      then

       A1: ((( All ((b 'imp' ( 'not' c)),PA,G)) . z) '&' (( All ((a 'imp' c),PA,G)) . z)) = TRUE by MARGREL1:def 20;

       A2:

      now

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

        then (( B_INF ((a 'imp' c),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((a 'imp' c),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

       A3:

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((b 'imp' ( 'not' c)) . x) = TRUE );

        then (( B_INF ((b 'imp' ( 'not' c)),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((b 'imp' ( 'not' c)),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

      for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((a 'imp' ( 'not' b)) . x) = TRUE

      proof

        let x be Element of Y;

        

         A4: ( 'not' (b . x)) = TRUE or ( 'not' (b . x)) = FALSE by XBOOLEAN:def 3;

        

         A5: ( 'not' (a . x)) = TRUE or ( 'not' (a . x)) = FALSE by XBOOLEAN:def 3;

        assume

         A6: x in ( EqClass (z,( CompF (PA,G))));

        then ((b 'imp' ( 'not' c)) . x) = TRUE by A3;

        then

         A7: (( 'not' (b . x)) 'or' (( 'not' c) . x)) = TRUE by BVFUNC_1:def 8;

        ((a 'imp' c) . x) = TRUE by A2, A6;

        then

         A8: (( 'not' (a . x)) 'or' (c . x)) = TRUE by BVFUNC_1:def 8;

        per cases by A7, A4, A8, A5, BINARITH: 3;

          suppose

           A9: ( 'not' (b . x)) = TRUE & ( 'not' (a . x)) = TRUE ;

          then (( 'not' b) . x) = TRUE by MARGREL1:def 19;

          

          hence ((a 'imp' ( 'not' b)) . x) = ( TRUE 'or' TRUE ) by A9, BVFUNC_1:def 8

          .= TRUE ;

        end;

          suppose ( 'not' (b . x)) = TRUE & (c . x) = TRUE ;

          then (( 'not' b) . x) = TRUE by MARGREL1:def 19;

          

          hence ((a 'imp' ( 'not' b)) . x) = (( 'not' (a . x)) 'or' TRUE ) by BVFUNC_1:def 8

          .= TRUE by BINARITH: 10;

        end;

          suppose (( 'not' c) . x) = TRUE & ( 'not' (a . x)) = TRUE ;

          

          hence ((a 'imp' ( 'not' b)) . x) = ( TRUE 'or' (( 'not' b) . x)) by BVFUNC_1:def 8

          .= TRUE by BINARITH: 10;

        end;

          suppose

           A10: (( 'not' c) . x) = TRUE & (c . x) = TRUE ;

          then ( 'not' (c . x)) = TRUE by MARGREL1:def 19;

          hence thesis by A10, MARGREL1: 11;

        end;

      end;

      then (( B_INF ((a 'imp' ( 'not' b)),( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 16;

      hence thesis by BVFUNC_2:def 9;

    end;

    theorem :: BVFUNC_3:35

    (( All ((b 'imp' c),PA,G)) '&' ( All ((a 'imp' ( 'not' c)),PA,G))) '<' ( All ((a 'imp' ( 'not' b)),PA,G))

    proof

      let z be Element of Y;

      assume ((( All ((b 'imp' c),PA,G)) '&' ( All ((a 'imp' ( 'not' c)),PA,G))) . z) = TRUE ;

      then

       A1: ((( All ((b 'imp' c),PA,G)) . z) '&' (( All ((a 'imp' ( 'not' c)),PA,G)) . z)) = TRUE by MARGREL1:def 20;

       A2:

      now

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

        then (( B_INF ((a 'imp' ( 'not' c)),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((a 'imp' ( 'not' c)),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

       A3:

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((b 'imp' c) . x) = TRUE );

        then (( B_INF ((b 'imp' c),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((b 'imp' c),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

      for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((a 'imp' ( 'not' b)) . x) = TRUE

      proof

        let x be Element of Y;

        

         A4: ( 'not' (b . x)) = TRUE or ( 'not' (b . x)) = FALSE by XBOOLEAN:def 3;

        

         A5: ( 'not' (a . x)) = TRUE or ( 'not' (a . x)) = FALSE by XBOOLEAN:def 3;

        assume

         A6: x in ( EqClass (z,( CompF (PA,G))));

        then ((b 'imp' c) . x) = TRUE by A3;

        then

         A7: (( 'not' (b . x)) 'or' (c . x)) = TRUE by BVFUNC_1:def 8;

        ((a 'imp' ( 'not' c)) . x) = TRUE by A2, A6;

        then

         A8: (( 'not' (a . x)) 'or' (( 'not' c) . x)) = TRUE by BVFUNC_1:def 8;

        per cases by A7, A4, A8, A5, BINARITH: 3;

          suppose

           A9: ( 'not' (b . x)) = TRUE & ( 'not' (a . x)) = TRUE ;

          then (( 'not' b) . x) = TRUE by MARGREL1:def 19;

          

          hence ((a 'imp' ( 'not' b)) . x) = ( TRUE 'or' TRUE ) by A9, BVFUNC_1:def 8

          .= TRUE ;

        end;

          suppose ( 'not' (b . x)) = TRUE & (( 'not' c) . x) = TRUE ;

          then (( 'not' b) . x) = TRUE by MARGREL1:def 19;

          

          hence ((a 'imp' ( 'not' b)) . x) = (( 'not' (a . x)) 'or' TRUE ) by BVFUNC_1:def 8

          .= TRUE by BINARITH: 10;

        end;

          suppose (c . x) = TRUE & ( 'not' (a . x)) = TRUE ;

          

          hence ((a 'imp' ( 'not' b)) . x) = ( TRUE 'or' (( 'not' b) . x)) by BVFUNC_1:def 8

          .= TRUE by BINARITH: 10;

        end;

          suppose

           A10: (c . x) = TRUE & (( 'not' c) . x) = TRUE ;

          then ( 'not' (c . x)) = TRUE by MARGREL1:def 19;

          hence thesis by A10, MARGREL1: 11;

        end;

      end;

      then (( B_INF ((a 'imp' ( 'not' b)),( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 16;

      hence thesis by BVFUNC_2:def 9;

    end;

    theorem :: BVFUNC_3:36

    (( All ((b 'imp' ( 'not' c)),PA,G)) '&' ( Ex ((a '&' c),PA,G))) '<' ( Ex ((a '&' ( 'not' b)),PA,G))

    proof

      let z be Element of Y;

      assume ((( All ((b 'imp' ( 'not' c)),PA,G)) '&' ( Ex ((a '&' c),PA,G))) . z) = TRUE ;

      then

       A1: ((( All ((b 'imp' ( 'not' c)),PA,G)) . z) '&' (( Ex ((a '&' c),PA,G)) . z)) = TRUE by MARGREL1:def 20;

      now

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

        then (( B_SUP ((a '&' c),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        then (( Ex ((a '&' c),PA,G)) . z) = FALSE by BVFUNC_2:def 10;

        hence contradiction by A1, MARGREL1: 12;

      end;

      then

      consider x1 be Element of Y such that

       A2: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A3: ((a '&' c) . x1) = TRUE ;

      

       A4: ((a . x1) '&' (c . x1)) = TRUE by A3, MARGREL1:def 20;

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((b 'imp' ( 'not' c)) . x) = TRUE );

        then (( B_INF ((b 'imp' ( 'not' c)),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((b 'imp' ( 'not' c)),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

      then ((b 'imp' ( 'not' c)) . x1) = TRUE by A2;

      then

       A5: (( 'not' (b . x1)) 'or' (( 'not' c) . x1)) = TRUE by BVFUNC_1:def 8;

      

       A6: ( 'not' (b . x1)) = TRUE or ( 'not' (b . x1)) = FALSE by XBOOLEAN:def 3;

      per cases by A5, A6, A4, BINARITH: 3, MARGREL1: 12;

        suppose

         A7: (a . x1) = TRUE & (c . x1) = TRUE & ( 'not' (b . x1)) = TRUE ;

        ((a '&' ( 'not' b)) . x1) = ((a . x1) '&' (( 'not' b) . x1)) by MARGREL1:def 20

        .= ( TRUE '&' TRUE ) by A7, MARGREL1:def 19

        .= TRUE ;

        then (( B_SUP ((a '&' ( 'not' b)),( CompF (PA,G)))) . z) = TRUE by A2, BVFUNC_1:def 17;

        hence thesis by BVFUNC_2:def 10;

      end;

        suppose

         A8: (a . x1) = TRUE & (c . x1) = TRUE & (( 'not' c) . x1) = TRUE ;

        then ( 'not' (c . x1)) = TRUE by MARGREL1:def 19;

        hence thesis by A8, MARGREL1: 11;

      end;

    end;

    theorem :: BVFUNC_3:37

    (( All ((b 'imp' c),PA,G)) '&' ( Ex ((a '&' ( 'not' c)),PA,G))) '<' ( Ex ((a '&' ( 'not' b)),PA,G))

    proof

      let z be Element of Y;

      assume ((( All ((b 'imp' c),PA,G)) '&' ( Ex ((a '&' ( 'not' c)),PA,G))) . z) = TRUE ;

      then

       A1: ((( All ((b 'imp' c),PA,G)) . z) '&' (( Ex ((a '&' ( 'not' c)),PA,G)) . z)) = TRUE by MARGREL1:def 20;

      now

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

        then (( B_SUP ((a '&' ( 'not' c)),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        then (( Ex ((a '&' ( 'not' c)),PA,G)) . z) = FALSE by BVFUNC_2:def 10;

        hence contradiction by A1, MARGREL1: 12;

      end;

      then

      consider x1 be Element of Y such that

       A2: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A3: ((a '&' ( 'not' c)) . x1) = TRUE ;

      

       A4: ((a . x1) '&' (( 'not' c) . x1)) = TRUE by A3, MARGREL1:def 20;

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((b 'imp' c) . x) = TRUE );

        then (( B_INF ((b 'imp' c),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((b 'imp' c),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

      then ((b 'imp' c) . x1) = TRUE by A2;

      then

       A5: (( 'not' (b . x1)) 'or' (c . x1)) = TRUE by BVFUNC_1:def 8;

      

       A6: ( 'not' (b . x1)) = TRUE or ( 'not' (b . x1)) = FALSE by XBOOLEAN:def 3;

      per cases by A5, A6, A4, BINARITH: 3, MARGREL1: 12;

        suppose

         A7: (a . x1) = TRUE & (( 'not' c) . x1) = TRUE & ( 'not' (b . x1)) = TRUE ;

        ((a '&' ( 'not' b)) . x1) = ((a . x1) '&' (( 'not' b) . x1)) by MARGREL1:def 20

        .= ( TRUE '&' TRUE ) by A7, MARGREL1:def 19

        .= TRUE ;

        then (( B_SUP ((a '&' ( 'not' b)),( CompF (PA,G)))) . z) = TRUE by A2, BVFUNC_1:def 17;

        hence thesis by BVFUNC_2:def 10;

      end;

        suppose

         A8: (a . x1) = TRUE & (( 'not' c) . x1) = TRUE & (c . x1) = TRUE ;

        then ( 'not' (c . x1)) = TRUE by MARGREL1:def 19;

        hence thesis by A8, MARGREL1: 11;

      end;

    end;

    theorem :: BVFUNC_3:38

    ((( Ex (c,PA,G)) '&' ( All ((c 'imp' b),PA,G))) '&' ( All ((c 'imp' a),PA,G))) '<' ( Ex ((a '&' b),PA,G))

    proof

      let z be Element of Y;

      assume (((( Ex (c,PA,G)) '&' ( All ((c 'imp' b),PA,G))) '&' ( All ((c 'imp' a),PA,G))) . z) = TRUE ;

      then

       A1: (((( Ex (c,PA,G)) '&' ( All ((c 'imp' b),PA,G))) . z) '&' (( All ((c 'imp' a),PA,G)) . z)) = TRUE by MARGREL1:def 20;

      then (((( Ex (c,PA,G)) . z) '&' (( All ((c 'imp' b),PA,G)) . z)) '&' (( All ((c 'imp' a),PA,G)) . z)) = TRUE by MARGREL1:def 20;

      then

       A2: ((( Ex (c,PA,G)) . z) '&' (( All ((c 'imp' b),PA,G)) . z)) = TRUE by MARGREL1: 12;

      now

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

        then (( B_SUP (c,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        then (( Ex (c,PA,G)) . z) = FALSE by BVFUNC_2:def 10;

        hence contradiction by A2, MARGREL1: 12;

      end;

      then

      consider x1 be Element of Y such that

       A3: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A4: (c . x1) = TRUE ;

      

       A5: ( 'not' (c . x1)) = TRUE or ( 'not' (c . x1)) = FALSE by XBOOLEAN:def 3;

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((c 'imp' b) . x) = TRUE );

        then (( B_INF ((c 'imp' b),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((c 'imp' b),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A2, MARGREL1: 12;

      end;

      then ((c 'imp' b) . x1) = TRUE by A3;

      then

       A6: (( 'not' (c . x1)) 'or' (b . x1)) = TRUE by BVFUNC_1:def 8;

      now

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

        then (( B_INF ((c 'imp' a),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((c 'imp' a),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

      then ((c 'imp' a) . x1) = TRUE by A3;

      then

       A7: (( 'not' (c . x1)) 'or' (a . x1)) = TRUE by BVFUNC_1:def 8;

      per cases by A7, A5, A6, BINARITH: 3;

        suppose ( 'not' (c . x1)) = TRUE ;

        hence thesis by A4, MARGREL1: 11;

      end;

        suppose ( 'not' (c . x1)) = TRUE & (b . x1) = TRUE ;

        hence thesis by A4, MARGREL1: 11;

      end;

        suppose (a . x1) = TRUE & ( 'not' (c . x1)) = TRUE ;

        hence thesis by A4, MARGREL1: 11;

      end;

        suppose (a . x1) = TRUE & (b . x1) = TRUE ;

        

        then ((a '&' b) . x1) = ( TRUE '&' TRUE ) by MARGREL1:def 20

        .= TRUE ;

        then (( B_SUP ((a '&' b),( CompF (PA,G)))) . z) = TRUE by A3, BVFUNC_1:def 17;

        hence thesis by BVFUNC_2:def 10;

      end;

    end;

    theorem :: BVFUNC_3:39

    (( All ((b 'imp' c),PA,G)) '&' ( All ((c 'imp' ( 'not' a)),PA,G))) '<' ( All ((a 'imp' ( 'not' b)),PA,G))

    proof

      let z be Element of Y;

      assume ((( All ((b 'imp' c),PA,G)) '&' ( All ((c 'imp' ( 'not' a)),PA,G))) . z) = TRUE ;

      then

       A1: ((( All ((b 'imp' c),PA,G)) . z) '&' (( All ((c 'imp' ( 'not' a)),PA,G)) . z)) = TRUE by MARGREL1:def 20;

       A2:

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((b 'imp' c) . x) = TRUE );

        then (( B_INF ((b 'imp' c),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((b 'imp' c),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

       A3:

      now

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

        then (( B_INF ((c 'imp' ( 'not' a)),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((c 'imp' ( 'not' a)),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

      for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((a 'imp' ( 'not' b)) . x) = TRUE

      proof

        let x be Element of Y;

        

         A4: ( 'not' (c . x)) = TRUE or ( 'not' (c . x)) = FALSE by XBOOLEAN:def 3;

        

         A5: ( 'not' (b . x)) = TRUE or ( 'not' (b . x)) = FALSE by XBOOLEAN:def 3;

        assume

         A6: x in ( EqClass (z,( CompF (PA,G))));

        then ((c 'imp' ( 'not' a)) . x) = TRUE by A3;

        then

         A7: (( 'not' (c . x)) 'or' (( 'not' a) . x)) = TRUE by BVFUNC_1:def 8;

        ((b 'imp' c) . x) = TRUE by A2, A6;

        then

         A8: (( 'not' (b . x)) 'or' (c . x)) = TRUE by BVFUNC_1:def 8;

        per cases by A7, A4, A8, A5, BINARITH: 3;

          suppose ( 'not' (c . x)) = TRUE & ( 'not' (b . x)) = TRUE ;

          then (( 'not' b) . x) = TRUE by MARGREL1:def 19;

          

          hence ((a 'imp' ( 'not' b)) . x) = (( 'not' (a . x)) 'or' TRUE ) by BVFUNC_1:def 8

          .= TRUE by BINARITH: 10;

        end;

          suppose ( 'not' (c . x)) = TRUE & (c . x) = TRUE ;

          hence thesis by MARGREL1: 11;

        end;

          suppose (( 'not' a) . x) = TRUE & ( 'not' (b . x)) = TRUE ;

          then (( 'not' b) . x) = TRUE by MARGREL1:def 19;

          

          hence ((a 'imp' ( 'not' b)) . x) = (( 'not' (a . x)) 'or' TRUE ) by BVFUNC_1:def 8

          .= TRUE by BINARITH: 10;

        end;

          suppose (( 'not' a) . x) = TRUE & (c . x) = TRUE ;

          then ( 'not' (a . x)) = TRUE by MARGREL1:def 19;

          

          hence ((a 'imp' ( 'not' b)) . x) = ( TRUE 'or' (( 'not' b) . x)) by BVFUNC_1:def 8

          .= TRUE by BINARITH: 10;

        end;

      end;

      then (( B_INF ((a 'imp' ( 'not' b)),( CompF (PA,G)))) . z) = TRUE by BVFUNC_1:def 16;

      hence thesis by BVFUNC_2:def 9;

    end;

    theorem :: BVFUNC_3:40

    ((( Ex (b,PA,G)) '&' ( All ((b 'imp' c),PA,G))) '&' ( All ((c 'imp' a),PA,G))) '<' ( Ex ((a '&' b),PA,G))

    proof

      let z be Element of Y;

      assume (((( Ex (b,PA,G)) '&' ( All ((b 'imp' c),PA,G))) '&' ( All ((c 'imp' a),PA,G))) . z) = TRUE ;

      then

       A1: (((( Ex (b,PA,G)) '&' ( All ((b 'imp' c),PA,G))) . z) '&' (( All ((c 'imp' a),PA,G)) . z)) = TRUE by MARGREL1:def 20;

      then (((( Ex (b,PA,G)) . z) '&' (( All ((b 'imp' c),PA,G)) . z)) '&' (( All ((c 'imp' a),PA,G)) . z)) = TRUE by MARGREL1:def 20;

      then

       A2: ((( Ex (b,PA,G)) . z) '&' (( All ((b 'imp' c),PA,G)) . z)) = TRUE by MARGREL1: 12;

      now

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

        then (( B_SUP (b,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        then (( Ex (b,PA,G)) . z) = FALSE by BVFUNC_2:def 10;

        hence contradiction by A2, MARGREL1: 12;

      end;

      then

      consider x1 be Element of Y such that

       A3: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A4: (b . x1) = TRUE ;

      

       A5: ( 'not' (c . x1)) = TRUE or ( 'not' (c . x1)) = FALSE by XBOOLEAN:def 3;

      now

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

        then (( B_INF ((c 'imp' a),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((c 'imp' a),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

      then ((c 'imp' a) . x1) = TRUE by A3;

      then

       A6: (( 'not' (c . x1)) 'or' (a . x1)) = TRUE by BVFUNC_1:def 8;

      

       A7: ( 'not' (b . x1)) = TRUE or ( 'not' (b . x1)) = FALSE by XBOOLEAN:def 3;

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((b 'imp' c) . x) = TRUE );

        then (( B_INF ((b 'imp' c),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((b 'imp' c),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A2, MARGREL1: 12;

      end;

      then ((b 'imp' c) . x1) = TRUE by A3;

      then

       A8: (( 'not' (b . x1)) 'or' (c . x1)) = TRUE by BVFUNC_1:def 8;

      per cases by A6, A5, A8, A7, BINARITH: 3;

        suppose ( 'not' (c . x1)) = TRUE & ( 'not' (b . x1)) = TRUE ;

        hence thesis by A4, MARGREL1: 11;

      end;

        suppose ( 'not' (c . x1)) = TRUE & (c . x1) = TRUE ;

        hence thesis by MARGREL1: 11;

      end;

        suppose (a . x1) = TRUE & ( 'not' (b . x1)) = TRUE ;

        hence thesis by A4, MARGREL1: 11;

      end;

        suppose (a . x1) = TRUE & (c . x1) = TRUE ;

        

        then ((a '&' b) . x1) = ( TRUE '&' TRUE ) by A4, MARGREL1:def 20

        .= TRUE ;

        then (( B_SUP ((a '&' b),( CompF (PA,G)))) . z) = TRUE by A3, BVFUNC_1:def 17;

        hence thesis by BVFUNC_2:def 10;

      end;

    end;

    theorem :: BVFUNC_3:41

    ((( Ex (c,PA,G)) '&' ( All ((b 'imp' ( 'not' c)),PA,G))) '&' ( All ((c 'imp' a),PA,G))) '<' ( Ex ((a '&' ( 'not' b)),PA,G))

    proof

      let z be Element of Y;

      assume (((( Ex (c,PA,G)) '&' ( All ((b 'imp' ( 'not' c)),PA,G))) '&' ( All ((c 'imp' a),PA,G))) . z) = TRUE ;

      then

       A1: (((( Ex (c,PA,G)) '&' ( All ((b 'imp' ( 'not' c)),PA,G))) . z) '&' (( All ((c 'imp' a),PA,G)) . z)) = TRUE by MARGREL1:def 20;

      then (((( Ex (c,PA,G)) . z) '&' (( All ((b 'imp' ( 'not' c)),PA,G)) . z)) '&' (( All ((c 'imp' a),PA,G)) . z)) = TRUE by MARGREL1:def 20;

      then

       A2: ((( Ex (c,PA,G)) . z) '&' (( All ((b 'imp' ( 'not' c)),PA,G)) . z)) = TRUE by MARGREL1: 12;

      now

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

        then (( B_SUP (c,( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 17;

        then (( Ex (c,PA,G)) . z) = FALSE by BVFUNC_2:def 10;

        hence contradiction by A2, MARGREL1: 12;

      end;

      then

      consider x1 be Element of Y such that

       A3: x1 in ( EqClass (z,( CompF (PA,G)))) and

       A4: (c . x1) = TRUE ;

      

       A5: ( 'not' (c . x1)) = TRUE or ( 'not' (c . x1)) = FALSE by XBOOLEAN:def 3;

      now

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

        then (( B_INF ((c 'imp' a),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((c 'imp' a),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A1, MARGREL1: 12;

      end;

      then ((c 'imp' a) . x1) = TRUE by A3;

      then

       A6: (( 'not' (c . x1)) 'or' (a . x1)) = TRUE by BVFUNC_1:def 8;

      

       A7: ( 'not' (b . x1)) = TRUE or ( 'not' (b . x1)) = FALSE by XBOOLEAN:def 3;

      now

        assume not (for x be Element of Y st x in ( EqClass (z,( CompF (PA,G)))) holds ((b 'imp' ( 'not' c)) . x) = TRUE );

        then (( B_INF ((b 'imp' ( 'not' c)),( CompF (PA,G)))) . z) = FALSE by BVFUNC_1:def 16;

        then (( All ((b 'imp' ( 'not' c)),PA,G)) . z) = FALSE by BVFUNC_2:def 9;

        hence contradiction by A2, MARGREL1: 12;

      end;

      then ((b 'imp' ( 'not' c)) . x1) = TRUE by A3;

      then

       A8: (( 'not' (b . x1)) 'or' (( 'not' c) . x1)) = TRUE by BVFUNC_1:def 8;

      per cases by A6, A5, A8, A7, BINARITH: 3;

        suppose ( 'not' (c . x1)) = TRUE & ( 'not' (b . x1)) = TRUE ;

        hence thesis by A4, MARGREL1: 11;

      end;

        suppose ( 'not' (c . x1)) = TRUE & (( 'not' c) . x1) = TRUE ;

        hence thesis by A4, MARGREL1: 11;

      end;

        suppose

         A9: (a . x1) = TRUE & ( 'not' (b . x1)) = TRUE ;

        ((a '&' ( 'not' b)) . x1) = ((a . x1) '&' (( 'not' b) . x1)) by MARGREL1:def 20

        .= ( TRUE '&' TRUE ) by A9, MARGREL1:def 19

        .= TRUE ;

        then (( B_SUP ((a '&' ( 'not' b)),( CompF (PA,G)))) . z) = TRUE by A3, BVFUNC_1:def 17;

        hence thesis by BVFUNC_2:def 10;

      end;

        suppose (a . x1) = TRUE & (( 'not' c) . x1) = TRUE ;

        then ( 'not' (c . x1)) = TRUE by MARGREL1:def 19;

        hence thesis by A4, MARGREL1: 11;

      end;

    end;