bvfunc_5.miz



    begin

    reserve Y for non empty set;

    theorem :: BVFUNC_5:1

    for a,b be Function of Y, BOOLEAN holds a = ( I_el Y) & b = ( I_el Y) iff (a '&' b) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      now

        assume

         A1: (a '&' b) = ( I_el Y);

        per cases ;

          suppose a = ( I_el Y) & b = ( I_el Y);

          hence a = ( I_el Y) & b = ( I_el Y);

        end;

          suppose a = ( I_el Y) & b <> ( I_el Y);

          hence a = ( I_el Y) & b = ( I_el Y) by A1, BVFUNC_1: 6;

        end;

          suppose a <> ( I_el Y) & b = ( I_el Y);

          hence a = ( I_el Y) & b = ( I_el Y) by A1, BVFUNC_1: 6;

        end;

          suppose

           A2: a <> ( I_el Y) & b <> ( I_el Y);

          for x be Element of Y holds (a . x) = TRUE

          proof

            let x be Element of Y;

            ((a '&' b) . x) = TRUE by A1, BVFUNC_1:def 11;

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

            hence thesis by MARGREL1: 12;

          end;

          hence a = ( I_el Y) & b = ( I_el Y) by A2, BVFUNC_1:def 11;

        end;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_5:2

    

     Th2: for b be Function of Y, BOOLEAN st (( I_el Y) 'imp' b) = ( I_el Y) holds b = ( I_el Y)

    proof

      set a = ( I_el Y);

      let b be Function of Y, BOOLEAN ;

      assume

       A1: (a 'imp' b) = ( I_el Y);

      for x be Element of Y holds (b . x) = TRUE

      proof

        let x be Element of Y;

        ((a 'imp' b) . x) = TRUE by A1, BVFUNC_1:def 11;

        then (a . x) = TRUE & (( 'not' (a . x)) 'or' (b . x)) = TRUE by BVFUNC_1:def 8, BVFUNC_1:def 11;

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

        hence thesis by BINARITH: 3;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:3

    for a,b be Function of Y, BOOLEAN st a = ( I_el Y) holds (a 'or' b) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      assume

       A1: a = ( I_el Y);

      for x be Element of Y holds ((a 'or' b) . x) = TRUE

      proof

        let x be Element of Y;

        (a . x) = TRUE by A1, BVFUNC_1:def 11;

        

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

        .= TRUE by BINARITH: 10;

        hence thesis;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:4

    for a,b be Function of Y, BOOLEAN st b = ( I_el Y) holds (a 'imp' b) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      assume

       A1: b = ( I_el Y);

      for x be Element of Y holds ((a 'imp' b) . x) = TRUE

      proof

        let x be Element of Y;

        (b . x) = TRUE by A1, BVFUNC_1:def 11;

        

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

        .= TRUE by BINARITH: 10;

        hence thesis;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:5

    for a,b be Function of Y, BOOLEAN st ( 'not' a) = ( I_el Y) holds (a 'imp' b) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      assume

       A1: ( 'not' a) = ( I_el Y);

      for x be Element of Y holds ((a 'imp' b) . x) = TRUE

      proof

        let x be Element of Y;

        (( 'not' a) . x) = TRUE by A1, BVFUNC_1:def 11;

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

        

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

        .= TRUE by BINARITH: 10;

        hence thesis;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:6

    for a be Function of Y, BOOLEAN holds ( 'not' (a '&' ( 'not' a))) = ( I_el Y)

    proof

      let a be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

      thus (( 'not' (a '&' ( 'not' a))) . x) = ( 'not' ((a '&' ( 'not' a)) . x)) by MARGREL1:def 19

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

      .= ( 'not' ((a . x) '&' ( 'not' (a . x)))) by MARGREL1:def 19

      .= TRUE by XBOOLEAN: 102

      .= (( I_el Y) . x) by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:7

    for a be Function of Y, BOOLEAN holds (a 'imp' a) = ( I_el Y)

    proof

      let a be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

       A1: ((a 'imp' a) . x) = (( 'not' (a . x)) 'or' (a . x)) & (( I_el Y) . x) = TRUE by BVFUNC_1:def 8, BVFUNC_1:def 11;

      

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

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence thesis by A1, BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          hence thesis by A2, A1, BINARITH: 10;

        end;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_5:8

    for a,b be Function of Y, BOOLEAN holds (a 'imp' b) = ( I_el Y) iff (( 'not' b) 'imp' ( 'not' a)) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

       A1:

      now

        assume

         A2: (( 'not' b) 'imp' ( 'not' a)) = ( I_el Y);

        for x be Element of Y holds ((a 'imp' b) . x) = TRUE

        proof

          let x be Element of Y;

          ((( 'not' b) 'imp' ( 'not' a)) . x) = TRUE by A2, BVFUNC_1:def 11;

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

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

          then

           A3: (( 'not' ( 'not' (b . x))) 'or' ( 'not' (a . x))) = TRUE by MARGREL1:def 19;

          

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

          now

            per cases by A3, A4, BINARITH: 3;

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

              

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

              .= TRUE by BINARITH: 10;

              hence thesis;

            end;

              case (b . x) = TRUE ;

              

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

              .= TRUE by BINARITH: 10;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        hence (a 'imp' b) = ( I_el Y) by BVFUNC_1:def 11;

      end;

      now

        assume

         A5: (a 'imp' b) = ( I_el Y);

        for x be Element of Y holds ((( 'not' b) 'imp' ( 'not' a)) . x) = TRUE

        proof

          let x be Element of Y;

          ((a 'imp' b) . x) = TRUE by A5, BVFUNC_1:def 11;

          then

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

          

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

          now

            per cases by A6, A7, BINARITH: 3;

              case

               A8: ( 'not' (a . x)) = TRUE ;

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

              .= (( 'not' (( 'not' b) . x)) 'or' TRUE ) by A8, MARGREL1:def 19

              .= TRUE by BINARITH: 10;

              hence thesis;

            end;

              case

               A9: (b . x) = TRUE ;

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

              

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

              .= TRUE by A9, BINARITH: 10;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        hence (( 'not' b) 'imp' ( 'not' a)) = ( I_el Y) by BVFUNC_1:def 11;

      end;

      hence thesis by A1;

    end;

    theorem :: BVFUNC_5:9

    for a,b,c be Function of Y, BOOLEAN st (a 'imp' b) = ( I_el Y) & (b 'imp' c) = ( I_el Y) holds (a 'imp' c) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      assume that

       A1: (a 'imp' b) = ( I_el Y) and

       A2: (b 'imp' c) = ( I_el Y);

      for x be Element of Y holds ((a 'imp' c) . x) = TRUE

      proof

        let x be Element of Y;

        

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

        

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

        ((b 'imp' c) . x) = TRUE by A2, BVFUNC_1:def 11;

        then

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

        ((a 'imp' b) . x) = TRUE by A1, BVFUNC_1:def 11;

        then

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

        

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

        now

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

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

            hence thesis by A4, BINARITH: 10;

          end;

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

            hence thesis by A4;

          end;

            case (b . x) = TRUE & ( 'not' (b . x)) = TRUE ;

            hence thesis by MARGREL1: 11;

          end;

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

            hence thesis by A4, BINARITH: 10;

          end;

        end;

        hence thesis;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:10

    for a,b be Function of Y, BOOLEAN st (a 'imp' b) = ( I_el Y) & (a 'imp' ( 'not' b)) = ( I_el Y) holds ( 'not' a) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      assume that

       A1: (a 'imp' b) = ( I_el Y) and

       A2: (a 'imp' ( 'not' b)) = ( I_el Y);

      for x be Element of Y holds (( 'not' a) . x) = TRUE

      proof

        let x be Element of Y;

        ((a 'imp' b) . x) = TRUE by A1, BVFUNC_1:def 11;

        then

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

        ((a 'imp' ( 'not' b)) . x) = TRUE by A2, BVFUNC_1:def 11;

        then

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

        

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

        now

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

            case ( 'not' (a . x)) = TRUE & ( 'not' (a . x)) = TRUE ;

            hence thesis by MARGREL1:def 19;

          end;

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

            hence thesis by MARGREL1:def 19;

          end;

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

            hence thesis by MARGREL1:def 19;

          end;

            case

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

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

            hence thesis by A6, MARGREL1: 11;

          end;

        end;

        hence thesis;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:11

    for a be Function of Y, BOOLEAN holds ((( 'not' a) 'imp' a) 'imp' a) = ( I_el Y)

    proof

      let a be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

       A1: ( 'not' (( 'not' (( 'not' a) . x)) 'or' (a . x))) = ( 'not' ((a . x) 'or' (a . x))) by MARGREL1:def 19

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

      

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

      .= (( 'not' (a . x)) 'or' (a . x)) by A1, BVFUNC_1:def 8;

      

       A3: (( I_el Y) . x) = TRUE by BVFUNC_1:def 11;

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence thesis by A2, A3, BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

          then (((( 'not' a) 'imp' a) 'imp' a) . x) = ( TRUE 'or' FALSE ) by A2, MARGREL1: 11

          .= TRUE by BINARITH: 10;

          hence thesis by BVFUNC_1:def 11;

        end;

      end;

      hence thesis;

    end;

    theorem :: BVFUNC_5:12

    for a,b,c be Function of Y, BOOLEAN holds ((a 'imp' b) 'imp' (( 'not' (b '&' c)) 'imp' ( 'not' (a '&' c)))) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

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

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

      

       A2: (( 'not' (a '&' c)) . x) = ((( 'not' a) 'or' ( 'not' c)) . x) by BVFUNC_1: 14

      .= ((( 'not' a) . x) 'or' (( 'not' c) . x)) by BVFUNC_1:def 4

      .= (( 'not' (a . x)) 'or' (( 'not' c) . x)) by MARGREL1:def 19

      .= (( 'not' (a . x)) 'or' ( 'not' (c . x))) by MARGREL1:def 19;

      now

        per cases by XBOOLEAN:def 3;

          case (c . x) = TRUE ;

          hence (( 'not' (c . x)) 'or' (c . x)) = TRUE by BINARITH: 10;

        end;

          case (c . x) = FALSE ;

          

          then (( 'not' (c . x)) 'or' (c . x)) = ( TRUE 'or' FALSE ) by MARGREL1: 11

          .= TRUE by BINARITH: 10;

          hence (( 'not' (c . x)) 'or' (c . x)) = TRUE ;

        end;

      end;

      then (( 'not' (a . x)) 'or' (( 'not' (c . x)) 'or' (c . x))) = TRUE by BINARITH: 10;

      then

       A3: (((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' (b . x)) '&' (( 'not' (a . x)) 'or' (( 'not' (c . x)) 'or' (c . x)))) = ((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' (b . x)) by MARGREL1: 14;

       A4:

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

        end;

      end;

       A5:

      now

        per cases by XBOOLEAN:def 3;

          case (b . x) = TRUE ;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

        end;

          case (b . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

        end;

      end;

      ( 'not' (( 'not' (b '&' c)) . x)) = ( 'not' ( 'not' ((b '&' c) . x))) by MARGREL1:def 19

      .= ((b . x) '&' (c . x)) by MARGREL1:def 20;

      

      then

       A6: (( 'not' (( 'not' (b '&' c)) . x)) 'or' (( 'not' (a '&' c)) . x)) = (((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' (b . x)) '&' ((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' (c . x))) by A2, XBOOLEAN: 9

      .= (((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' (b . x)) '&' (( 'not' (a . x)) 'or' (( 'not' (c . x)) 'or' (c . x)))) by BINARITH: 11;

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

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

      

      then (( 'not' ((a 'imp' b) . x)) 'or' (( 'not' (( 'not' (b '&' c)) . x)) 'or' (( 'not' (a '&' c)) . x))) = ((((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' (b . x)) 'or' (a . x)) '&' (((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' (b . x)) 'or' ( 'not' (b . x)))) by A6, A3, XBOOLEAN: 9

      .= ((((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' (b . x)) 'or' (a . x)) '&' ((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' ((b . x) 'or' ( 'not' (b . x))))) by BINARITH: 11

      .= ((((( 'not' (c . x)) 'or' ( 'not' (a . x))) 'or' (a . x)) 'or' (b . x)) '&' ((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' ((b . x) 'or' ( 'not' (b . x))))) by BINARITH: 11

      .= (((( 'not' (c . x)) 'or' (( 'not' (a . x)) 'or' (a . x))) 'or' (b . x)) '&' ((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' ((b . x) 'or' ( 'not' (b . x))))) by BINARITH: 11;

      

      then (( 'not' ((a 'imp' b) . x)) 'or' (( 'not' (( 'not' (b '&' c)) . x)) 'or' (( 'not' (a '&' c)) . x))) = (( TRUE 'or' (b . x)) '&' ((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' TRUE )) by A4, A5, BINARITH: 10

      .= ( TRUE '&' ((( 'not' (a . x)) 'or' ( 'not' (c . x))) 'or' TRUE )) by BINARITH: 10

      .= ( TRUE '&' TRUE ) by BINARITH: 10

      .= TRUE ;

      hence thesis by A1, BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:13

    for a,b,c be Function of Y, BOOLEAN holds ((a 'imp' b) 'imp' ((b 'imp' c) 'imp' (a 'imp' c))) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      let x be Element of Y;

      

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

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

      

       A2: ( 'not' ((b 'imp' c) . x)) = ( 'not' (( 'not' (b . x)) 'or' (c . x))) by BVFUNC_1:def 8

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

       A3:

      now

        per cases by XBOOLEAN:def 3;

          case (b . x) = TRUE ;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

        end;

          case (b . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

        end;

      end;

      

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

       A5:

      now

        per cases by XBOOLEAN:def 3;

          case (c . x) = TRUE ;

          hence (( 'not' (c . x)) 'or' (c . x)) = TRUE by BINARITH: 10;

        end;

          case (c . x) = FALSE ;

          

          then (( 'not' (c . x)) 'or' (c . x)) = ( TRUE 'or' FALSE ) by MARGREL1: 11

          .= TRUE by BINARITH: 10;

          hence (( 'not' (c . x)) 'or' (c . x)) = TRUE ;

        end;

      end;

       A6:

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

        end;

      end;

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

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

      

      then (( 'not' ((a 'imp' b) . x)) 'or' (( 'not' ((b 'imp' c) . x)) 'or' ((a 'imp' c) . x))) = (((((b . x) '&' ( 'not' (c . x))) 'or' (( 'not' (a . x)) 'or' (c . x))) 'or' (a . x)) '&' ((((b . x) '&' ( 'not' (c . x))) 'or' (( 'not' (a . x)) 'or' (c . x))) 'or' ( 'not' (b . x)))) by A2, A4, XBOOLEAN: 9

      .= ((((b . x) '&' ( 'not' (c . x))) 'or' (((c . x) 'or' ( 'not' (a . x))) 'or' (a . x))) '&' ((((b . x) '&' ( 'not' (c . x))) 'or' (( 'not' (a . x)) 'or' (c . x))) 'or' ( 'not' (b . x)))) by BINARITH: 11

      .= ((((b . x) '&' ( 'not' (c . x))) 'or' ((c . x) 'or' (( 'not' (a . x)) 'or' (a . x)))) '&' (((( 'not' (a . x)) 'or' (c . x)) 'or' ((b . x) '&' ( 'not' (c . x)))) 'or' ( 'not' (b . x)))) by BINARITH: 11

      .= ((((b . x) '&' ( 'not' (c . x))) 'or' ((c . x) 'or' (( 'not' (a . x)) 'or' (a . x)))) '&' ((( 'not' (a . x)) 'or' (c . x)) 'or' ((( 'not' (c . x)) '&' (b . x)) 'or' ( 'not' (b . x))))) by BINARITH: 11

      .= ((((b . x) '&' ( 'not' (c . x))) 'or' ((c . x) 'or' (( 'not' (a . x)) 'or' (a . x)))) '&' ((( 'not' (a . x)) 'or' (c . x)) 'or' ((( 'not' (b . x)) 'or' ( 'not' (c . x))) '&' (( 'not' (b . x)) 'or' (b . x))))) by XBOOLEAN: 9

      .= ((((b . x) '&' ( 'not' (c . x))) 'or' TRUE ) '&' ((( 'not' (a . x)) 'or' (c . x)) 'or' ((( 'not' (b . x)) 'or' ( 'not' (c . x))) '&' TRUE ))) by A3, A6, BINARITH: 10

      .= ( TRUE '&' ((( 'not' (a . x)) 'or' (c . x)) 'or' ((( 'not' (b . x)) 'or' ( 'not' (c . x))) '&' TRUE ))) by BINARITH: 10

      .= ((( 'not' (a . x)) 'or' (c . x)) 'or' ( TRUE '&' (( 'not' (b . x)) 'or' ( 'not' (c . x))))) by MARGREL1: 14

      .= ((( 'not' (a . x)) 'or' (c . x)) 'or' (( 'not' (c . x)) 'or' ( 'not' (b . x)))) by MARGREL1: 14

      .= (((( 'not' (a . x)) 'or' (c . x)) 'or' ( 'not' (c . x))) 'or' ( 'not' (b . x))) by BINARITH: 11

      .= ((( 'not' (a . x)) 'or' TRUE ) 'or' ( 'not' (b . x))) by A5, BINARITH: 11

      .= ( TRUE 'or' ( 'not' (b . x))) by BINARITH: 10

      .= TRUE by BINARITH: 10;

      hence thesis by A1, BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:14

    

     Th14: for a,b,c be Function of Y, BOOLEAN st (a 'imp' b) = ( I_el Y) holds ((b 'imp' c) 'imp' (a 'imp' c)) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      assume

       A1: (a 'imp' b) = ( I_el Y);

      for x be Element of Y holds (((b 'imp' c) 'imp' (a 'imp' c)) . x) = TRUE

      proof

        let x be Element of Y;

        

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

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

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

         A3:

        now

          per cases by XBOOLEAN:def 3;

            case (c . x) = TRUE ;

            hence (( 'not' (c . x)) 'or' (c . x)) = TRUE by BINARITH: 10;

          end;

            case (c . x) = FALSE ;

            

            then (( 'not' (c . x)) 'or' (c . x)) = ( TRUE 'or' FALSE ) by MARGREL1: 11

            .= TRUE by BINARITH: 10;

            hence (( 'not' (c . x)) 'or' (c . x)) = TRUE ;

          end;

        end;

        ((a 'imp' b) . x) = TRUE by A1, BVFUNC_1:def 11;

        then

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

        

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

        now

          per cases by A4, A5, BINARITH: 3;

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

            

            then (((b 'imp' c) 'imp' (a 'imp' c)) . x) = ( TRUE 'or' ((b . x) '&' ( 'not' (c . x)))) by A2, BINARITH: 10

            .= TRUE by BINARITH: 10;

            hence thesis;

          end;

            case (b . x) = TRUE ;

            

            then (((b 'imp' c) 'imp' (a 'imp' c)) . x) = ((( 'not' (a . x)) 'or' (c . x)) 'or' ( 'not' (c . x))) by A2, MARGREL1: 14

            .= (( 'not' (a . x)) 'or' TRUE ) by A3, BINARITH: 11

            .= TRUE by BINARITH: 10;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:15

    

     Th15: for a,b be Function of Y, BOOLEAN holds (b 'imp' (a 'imp' b)) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        per cases by XBOOLEAN:def 3;

          case (b . x) = TRUE ;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

        end;

          case (b . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

        end;

      end;

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

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

      .= ( TRUE 'or' ( 'not' (a . x))) by A1, BINARITH: 11

      .= TRUE by BINARITH: 10;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:16

    for a,b,c be Function of Y, BOOLEAN holds (((a 'imp' b) 'imp' c) 'imp' (b 'imp' c)) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      (b 'imp' (a 'imp' b)) = ( I_el Y) by Th15;

      hence thesis by Th14;

    end;

    theorem :: BVFUNC_5:17

    for a,b be Function of Y, BOOLEAN holds (b 'imp' ((b 'imp' a) 'imp' a)) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        per cases by XBOOLEAN:def 3;

          case (b . x) = TRUE ;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

        end;

          case (b . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

        end;

      end;

       A2:

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

        end;

      end;

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

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

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

      .= (( 'not' (b . x)) 'or' (((a . x) 'or' (b . x)) '&' TRUE )) by A2, XBOOLEAN: 9

      .= (( 'not' (b . x)) 'or' ((a . x) 'or' (b . x))) by MARGREL1: 14

      .= ((( 'not' (b . x)) 'or' (b . x)) 'or' (a . x)) by BINARITH: 11

      .= TRUE by A1, BINARITH: 10;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:18

    for a,b,c be Function of Y, BOOLEAN holds ((c 'imp' (b 'imp' a)) 'imp' (b 'imp' (c 'imp' a))) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        per cases by XBOOLEAN:def 3;

          case (b . x) = TRUE ;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

        end;

          case (b . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

        end;

      end;

       A2:

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

        end;

      end;

       A3:

      now

        per cases by XBOOLEAN:def 3;

          case (c . x) = TRUE ;

          hence (( 'not' (c . x)) 'or' (c . x)) = TRUE by BINARITH: 10;

        end;

          case (c . x) = FALSE ;

          

          then (( 'not' (c . x)) 'or' (c . x)) = ( TRUE 'or' FALSE ) by MARGREL1: 11

          .= TRUE by BINARITH: 10;

          hence (( 'not' (c . x)) 'or' (c . x)) = TRUE ;

        end;

      end;

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

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

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

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

      .= (((c . x) '&' (( 'not' ( 'not' (b . x))) '&' ( 'not' (a . x)))) 'or' (( 'not' (b . x)) 'or' (( 'not' (c . x)) 'or' (a . x)))) by BVFUNC_1:def 8

      .= (((( 'not' (c . x)) 'or' (a . x)) 'or' ( 'not' (b . x))) 'or' ((b . x) '&' ((c . x) '&' ( 'not' (a . x))))) by MARGREL1: 16

      .= ((((( 'not' (c . x)) 'or' (a . x)) 'or' ( 'not' (b . x))) 'or' (b . x)) '&' (((( 'not' (c . x)) 'or' (a . x)) 'or' ( 'not' (b . x))) 'or' ((c . x) '&' ( 'not' (a . x))))) by XBOOLEAN: 9

      .= (((( 'not' (c . x)) 'or' (a . x)) 'or' TRUE ) '&' (((( 'not' (c . x)) 'or' (a . x)) 'or' ( 'not' (b . x))) 'or' ((c . x) '&' ( 'not' (a . x))))) by A1, BINARITH: 11

      .= ( TRUE '&' (((( 'not' (c . x)) 'or' (a . x)) 'or' ( 'not' (b . x))) 'or' ((c . x) '&' ( 'not' (a . x))))) by BINARITH: 10

      .= (((( 'not' (c . x)) 'or' (a . x)) 'or' ( 'not' (b . x))) 'or' ((c . x) '&' ( 'not' (a . x)))) by MARGREL1: 14

      .= ((((a . x) 'or' ( 'not' (b . x))) 'or' ( 'not' (c . x))) 'or' ((c . x) '&' ( 'not' (a . x)))) by BINARITH: 11

      .= (((a . x) 'or' ( 'not' (b . x))) 'or' (( 'not' (c . x)) 'or' ((c . x) '&' ( 'not' (a . x))))) by BINARITH: 11

      .= (((a . x) 'or' ( 'not' (b . x))) 'or' ( TRUE '&' (( 'not' (c . x)) 'or' ( 'not' (a . x))))) by A3, XBOOLEAN: 9

      .= ((( 'not' (b . x)) 'or' (a . x)) 'or' (( 'not' (c . x)) 'or' ( 'not' (a . x)))) by MARGREL1: 14

      .= (((( 'not' (b . x)) 'or' (a . x)) 'or' ( 'not' (a . x))) 'or' ( 'not' (c . x))) by BINARITH: 11

      .= ((( 'not' (b . x)) 'or' TRUE ) 'or' ( 'not' (c . x))) by A2, BINARITH: 11

      .= ( TRUE 'or' ( 'not' (c . x))) by BINARITH: 10

      .= TRUE by BINARITH: 10;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:19

    for a,b,c be Function of Y, BOOLEAN holds ((b 'imp' c) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

        end;

      end;

       A2:

      now

        per cases by XBOOLEAN:def 3;

          case (b . x) = TRUE ;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

        end;

          case (b . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

        end;

      end;

       A3:

      now

        per cases by XBOOLEAN:def 3;

          case (c . x) = TRUE ;

          hence (( 'not' (c . x)) 'or' (c . x)) = TRUE by BINARITH: 10;

        end;

          case (c . x) = FALSE ;

          

          then (( 'not' (c . x)) 'or' (c . x)) = ( TRUE 'or' FALSE ) by MARGREL1: 11

          .= TRUE by BINARITH: 10;

          hence (( 'not' (c . x)) 'or' (c . x)) = TRUE ;

        end;

      end;

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

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

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

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

      .= (((b . x) '&' ( 'not' (c . x))) 'or' ((( 'not' ( 'not' (a . x))) '&' ( 'not' (b . x))) 'or' (( 'not' (a . x)) 'or' (c . x)))) by BVFUNC_1:def 8

      .= (((((a . x) '&' ( 'not' (b . x))) 'or' (( 'not' (a . x)) 'or' (c . x))) 'or' ( 'not' (c . x))) '&' ((((a . x) '&' ( 'not' (b . x))) 'or' (( 'not' (a . x)) 'or' (c . x))) 'or' (b . x))) by XBOOLEAN: 9

      .= ((((a . x) '&' ( 'not' (b . x))) 'or' ((( 'not' (a . x)) 'or' (c . x)) 'or' ( 'not' (c . x)))) '&' ((((a . x) '&' ( 'not' (b . x))) 'or' (( 'not' (a . x)) 'or' (c . x))) 'or' (b . x))) by BINARITH: 11

      .= ((((a . x) '&' ( 'not' (b . x))) 'or' (( 'not' (a . x)) 'or' TRUE )) '&' ((((a . x) '&' ( 'not' (b . x))) 'or' (( 'not' (a . x)) 'or' (c . x))) 'or' (b . x))) by A3, BINARITH: 11

      .= ((((a . x) '&' ( 'not' (b . x))) 'or' TRUE ) '&' ((((a . x) '&' ( 'not' (b . x))) 'or' (( 'not' (a . x)) 'or' (c . x))) 'or' (b . x))) by BINARITH: 10

      .= ( TRUE '&' ((((a . x) '&' ( 'not' (b . x))) 'or' (( 'not' (a . x)) 'or' (c . x))) 'or' (b . x))) by BINARITH: 10

      .= (((( 'not' (b . x)) '&' (a . x)) 'or' (( 'not' (a . x)) 'or' (c . x))) 'or' (b . x)) by MARGREL1: 14

      .= ((((( 'not' (a . x)) 'or' (c . x)) 'or' ( 'not' (b . x))) '&' ((( 'not' (a . x)) 'or' (c . x)) 'or' (a . x))) 'or' (b . x)) by XBOOLEAN: 9

      .= ((((( 'not' (a . x)) 'or' (c . x)) 'or' ( 'not' (b . x))) '&' ((c . x) 'or' (( 'not' (a . x)) 'or' (a . x)))) 'or' (b . x)) by BINARITH: 11

      .= ((((( 'not' (a . x)) 'or' (c . x)) 'or' ( 'not' (b . x))) '&' TRUE ) 'or' (b . x)) by A1, BINARITH: 10

      .= (((( 'not' (a . x)) 'or' (c . x)) 'or' ( 'not' (b . x))) 'or' (b . x)) by MARGREL1: 14

      .= ((( 'not' (a . x)) 'or' (c . x)) 'or' TRUE ) by A2, BINARITH: 11

      .= TRUE by BINARITH: 10;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:20

    for a,b,c be Function of Y, BOOLEAN holds ((b 'imp' (b 'imp' c)) 'imp' (b 'imp' c)) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        per cases by XBOOLEAN:def 3;

          case (b . x) = TRUE ;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

        end;

          case (b . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

        end;

      end;

       A2:

      now

        per cases by XBOOLEAN:def 3;

          case (c . x) = TRUE ;

          hence (( 'not' (c . x)) 'or' (c . x)) = TRUE by BINARITH: 10;

        end;

          case (c . x) = FALSE ;

          

          then (( 'not' (c . x)) 'or' (c . x)) = ( TRUE 'or' FALSE ) by MARGREL1: 11

          .= TRUE by BINARITH: 10;

          hence (( 'not' (c . x)) 'or' (c . x)) = TRUE ;

        end;

      end;

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

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

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

      .= (((b . x) '&' (( 'not' ( 'not' (b . x))) '&' ( 'not' (c . x)))) 'or' (( 'not' (b . x)) 'or' (c . x))) by BVFUNC_1:def 8

      .= ((((b . x) '&' (b . x)) '&' ( 'not' (c . x))) 'or' (( 'not' (b . x)) 'or' (c . x))) by MARGREL1: 16

      .= ((((c . x) 'or' ( 'not' (b . x))) 'or' (b . x)) '&' ((( 'not' (b . x)) 'or' (c . x)) 'or' ( 'not' (c . x)))) by XBOOLEAN: 9

      .= (((c . x) 'or' TRUE ) '&' ((( 'not' (b . x)) 'or' (c . x)) 'or' ( 'not' (c . x)))) by A1, BINARITH: 11

      .= ( TRUE '&' ((( 'not' (b . x)) 'or' (c . x)) 'or' ( 'not' (c . x)))) by BINARITH: 10

      .= ((( 'not' (b . x)) 'or' (c . x)) 'or' ( 'not' (c . x))) by MARGREL1: 14

      .= (( 'not' (b . x)) 'or' TRUE ) by A2, BINARITH: 11

      .= TRUE by BINARITH: 10;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:21

    

     Th21: for a,b,c be Function of Y, BOOLEAN holds ((a 'imp' (b 'imp' c)) 'imp' ((a 'imp' b) 'imp' (a 'imp' c))) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

        end;

      end;

       A2:

      now

        per cases by XBOOLEAN:def 3;

          case (c . x) = TRUE ;

          hence (( 'not' (c . x)) 'or' (c . x)) = TRUE by BINARITH: 10;

        end;

          case (c . x) = FALSE ;

          

          then (( 'not' (c . x)) 'or' (c . x)) = ( TRUE 'or' FALSE ) by MARGREL1: 11

          .= TRUE by BINARITH: 10;

          hence (( 'not' (c . x)) 'or' (c . x)) = TRUE ;

        end;

      end;

       A3:

      now

        per cases by XBOOLEAN:def 3;

          case (b . x) = TRUE ;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

        end;

          case (b . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

        end;

      end;

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

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

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

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

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

      .= ((( 'not' ( 'not' (a . x))) '&' (( 'not' ( 'not' (b . x))) '&' ( 'not' (c . x)))) 'or' ((( 'not' ( 'not' (a . x))) '&' ( 'not' (b . x))) 'or' (( 'not' (a . x)) 'or' (c . x)))) by BVFUNC_1:def 8

      .= (((a . x) '&' ((b . x) '&' ( 'not' (c . x)))) 'or' ((((c . x) 'or' ( 'not' (a . x))) 'or' (a . x)) '&' (((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))))) by XBOOLEAN: 9

      .= (((a . x) '&' ((b . x) '&' ( 'not' (c . x)))) 'or' (((c . x) 'or' TRUE ) '&' (((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))))) by A1, BINARITH: 11

      .= (((a . x) '&' ((b . x) '&' ( 'not' (c . x)))) 'or' ( TRUE '&' (((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))))) by BINARITH: 10

      .= ((((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))) 'or' ((a . x) '&' ((b . x) '&' ( 'not' (c . x))))) by MARGREL1: 14

      .= (((((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))) 'or' (a . x)) '&' ((((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))) 'or' ((b . x) '&' ( 'not' (c . x))))) by XBOOLEAN: 9

      .= (((((c . x) 'or' ( 'not' (a . x))) 'or' (a . x)) 'or' ( 'not' (b . x))) '&' ((((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))) 'or' ((b . x) '&' ( 'not' (c . x))))) by BINARITH: 11

      .= ((((c . x) 'or' TRUE ) 'or' ( 'not' (b . x))) '&' ((((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))) 'or' ((b . x) '&' ( 'not' (c . x))))) by A1, BINARITH: 11

      .= (( TRUE 'or' ( 'not' (b . x))) '&' ((((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))) 'or' ((b . x) '&' ( 'not' (c . x))))) by BINARITH: 10

      .= ( TRUE '&' ((((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))) 'or' ((b . x) '&' ( 'not' (c . x))))) by BINARITH: 10

      .= ((((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))) 'or' ((b . x) '&' ( 'not' (c . x)))) by MARGREL1: 14

      .= (((((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))) 'or' (b . x)) '&' ((((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))) 'or' ( 'not' (c . x)))) by XBOOLEAN: 9

      .= ((((c . x) 'or' ( 'not' (a . x))) 'or' TRUE ) '&' ((((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))) 'or' ( 'not' (c . x)))) by A3, BINARITH: 11

      .= ( TRUE '&' ((((c . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x))) 'or' ( 'not' (c . x)))) by BINARITH: 10

      .= ((( 'not' (b . x)) 'or' ((c . x) 'or' ( 'not' (a . x)))) 'or' ( 'not' (c . x))) by MARGREL1: 14

      .= (((( 'not' (b . x)) 'or' ( 'not' (a . x))) 'or' (c . x)) 'or' ( 'not' (c . x))) by BINARITH: 11

      .= ((( 'not' (b . x)) 'or' ( 'not' (a . x))) 'or' TRUE ) by A2, BINARITH: 11

      .= TRUE by BINARITH: 10;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:22

    for a,b be Function of Y, BOOLEAN holds a = ( I_el Y) implies ((a 'imp' b) 'imp' b) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      assume

       A1: a = ( I_el Y);

      for x be Element of Y holds (((a 'imp' b) 'imp' b) . x) = TRUE

      proof

        let x be Element of Y;

         A2:

        now

          per cases by XBOOLEAN:def 3;

            case (b . x) = TRUE ;

            hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

          end;

            case (b . x) = FALSE ;

            

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

            .= TRUE by BINARITH: 10;

            hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

          end;

        end;

        

         A3: (a . x) = TRUE by A1, BVFUNC_1:def 11;

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

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

        .= (((b . x) 'or' TRUE ) '&' TRUE ) by A3, A2, XBOOLEAN: 9

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

        .= TRUE by BINARITH: 10;

        hence thesis;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:23

    for a,b,c be Function of Y, BOOLEAN holds (c 'imp' (b 'imp' a)) = ( I_el Y) implies (b 'imp' (c 'imp' a)) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      assume

       A1: (c 'imp' (b 'imp' a)) = ( I_el Y);

      for x be Element of Y holds ((b 'imp' (c 'imp' a)) . x) = TRUE

      proof

        let x be Element of Y;

        ((c 'imp' (b 'imp' a)) . x) = TRUE by A1, BVFUNC_1:def 11;

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

        then

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

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

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

        .= TRUE by A2, BINARITH: 11;

        hence thesis;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:24

    for a,b,c be Function of Y, BOOLEAN holds (c 'imp' (b 'imp' a)) = ( I_el Y) & b = ( I_el Y) implies (c 'imp' a) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      assume that

       A1: (c 'imp' (b 'imp' a)) = ( I_el Y) and

       A2: b = ( I_el Y);

      for x be Element of Y holds ((c 'imp' a) . x) = TRUE

      proof

        let x be Element of Y;

        ((c 'imp' (b 'imp' a)) . x) = TRUE by A1, BVFUNC_1:def 11;

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

        then

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

        (( 'not' (c . x)) 'or' ( FALSE 'or' (a . x))) = TRUE by A3, A2, BVFUNC_1:def 11, MARGREL1: 11;

        then (( 'not' (c . x)) 'or' (a . x)) = TRUE by BINARITH: 3;

        hence thesis by BVFUNC_1:def 8;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:25

    

     Th25: for a be Function of Y, BOOLEAN holds (( I_el Y) 'imp' (( I_el Y) 'imp' a)) = ( I_el Y) implies a = ( I_el Y)

    proof

      let a be Function of Y, BOOLEAN ;

      assume (( I_el Y) 'imp' (( I_el Y) 'imp' a)) = ( I_el Y);

      then (( I_el Y) 'imp' a) = ( I_el Y) by Th2;

      hence thesis by Th2;

    end;

    theorem :: BVFUNC_5:26

    for b,c be Function of Y, BOOLEAN holds (b 'imp' (b 'imp' c)) = ( I_el Y) implies (b 'imp' c) = ( I_el Y)

    proof

      let b,c be Function of Y, BOOLEAN ;

      assume

       A1: (b 'imp' (b 'imp' c)) = ( I_el Y);

      for x be Element of Y holds ((b 'imp' c) . x) = TRUE

      proof

        let x be Element of Y;

        

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

        ((b 'imp' (b 'imp' c)) . x) = TRUE by A1, BVFUNC_1:def 11;

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

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

        then

         A3: ((( 'not' (b . x)) 'or' ( 'not' (b . x))) 'or' (c . x)) = TRUE by BINARITH: 11;

        

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

        now

          per cases by A3, A4, BINARITH: 3;

            case ( 'not' (b . x)) = TRUE ;

            hence thesis by A2, BINARITH: 10;

          end;

            case (c . x) = TRUE ;

            hence thesis by A2, BINARITH: 10;

          end;

        end;

        hence thesis;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:27

    for a,b,c be Function of Y, BOOLEAN holds (a 'imp' (b 'imp' c)) = ( I_el Y) implies ((a 'imp' b) 'imp' (a 'imp' c)) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      assume

       A1: (a 'imp' (b 'imp' c)) = ( I_el Y);

      for x be Element of Y holds (((a 'imp' b) 'imp' (a 'imp' c)) . x) = TRUE

      proof

        let x be Element of Y;

         A2:

        now

          per cases by XBOOLEAN:def 3;

            case (a . x) = TRUE ;

            hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

          end;

            case (a . x) = FALSE ;

            

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

            .= TRUE by BINARITH: 10;

            hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

          end;

        end;

        ((a 'imp' (b 'imp' c)) . x) = TRUE by A1, BVFUNC_1:def 11;

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

        then

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

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

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

        .= ((( 'not' ( 'not' (a . x))) '&' ( 'not' (b . x))) 'or' (( 'not' (a . x)) 'or' (c . x))) by BVFUNC_1:def 8

        .= (((( 'not' (a . x)) 'or' (c . x)) 'or' (a . x)) '&' ((( 'not' (a . x)) 'or' (c . x)) 'or' ( 'not' (b . x)))) by XBOOLEAN: 9

        .= ( TRUE '&' ((( 'not' (a . x)) 'or' (c . x)) 'or' (a . x))) by A3, BINARITH: 11

        .= (((c . x) 'or' ( 'not' (a . x))) 'or' (a . x)) by MARGREL1: 14

        .= ((c . x) 'or' TRUE ) by A2, BINARITH: 11

        .= TRUE by BINARITH: 10;

        hence thesis;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:28

    for a,b,c be Function of Y, BOOLEAN holds (a 'imp' (b 'imp' c)) = ( I_el Y) & (a 'imp' b) = ( I_el Y) implies (a 'imp' c) = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      assume (a 'imp' (b 'imp' c)) = ( I_el Y) & (a 'imp' b) = ( I_el Y);

      then (( I_el Y) 'imp' (( I_el Y) 'imp' (a 'imp' c))) = ( I_el Y) by Th21;

      hence thesis by Th25;

    end;

    theorem :: BVFUNC_5:29

    for a,b,c be Function of Y, BOOLEAN holds (a 'imp' (b 'imp' c)) = ( I_el Y) & (a 'imp' b) = ( I_el Y) & a = ( I_el Y) implies c = ( I_el Y)

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      assume that

       A1: (a 'imp' (b 'imp' c)) = ( I_el Y) and

       A2: (a 'imp' b) = ( I_el Y) and

       A3: a = ( I_el Y);

      for x be Element of Y holds (c . x) = TRUE

      proof

        let x be Element of Y;

        ((a 'imp' (b 'imp' c)) . x) = TRUE by A1, BVFUNC_1:def 11;

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

        then

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

        ((a 'imp' b) . x) = TRUE by A2, BVFUNC_1:def 11;

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

        then ( FALSE 'or' (b . x)) = TRUE by A3, BVFUNC_1:def 11, MARGREL1: 11;

        then (b . x) = TRUE by BINARITH: 3;

        then ( FALSE 'or' (( 'not' TRUE ) 'or' (c . x))) = TRUE by A4, A3, BVFUNC_1:def 11, MARGREL1: 11;

        then ( FALSE 'or' ( FALSE 'or' (c . x))) = TRUE by MARGREL1: 11;

        then ( FALSE 'or' (c . x)) = TRUE by BINARITH: 3;

        hence thesis by BINARITH: 3;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:30

    for a,b,c,d be Function of Y, BOOLEAN holds (a 'imp' (b 'imp' c)) = ( I_el Y) & (a 'imp' (c 'imp' d)) = ( I_el Y) implies (a 'imp' (b 'imp' d)) = ( I_el Y)

    proof

      let a,b,c,d be Function of Y, BOOLEAN ;

      assume that

       A1: (a 'imp' (b 'imp' c)) = ( I_el Y) and

       A2: (a 'imp' (c 'imp' d)) = ( I_el Y);

      for x be Element of Y holds ((a 'imp' (b 'imp' d)) . x) = TRUE

      proof

        let x be Element of Y;

        

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

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

        ((a 'imp' (c 'imp' d)) . x) = TRUE by A2, BVFUNC_1:def 11;

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

        then

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

        ((a 'imp' (b 'imp' c)) . x) = TRUE by A1, BVFUNC_1:def 11;

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

        then

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

        

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

        now

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

            case ( 'not' (a . x)) = TRUE & ( 'not' (a . x)) = TRUE ;

            hence thesis by A3, BINARITH: 10;

          end;

            case ( 'not' (a . x)) = TRUE & (( 'not' (c . x)) 'or' (d . x)) = TRUE ;

            hence thesis by A3, BINARITH: 10;

          end;

            case (( 'not' (b . x)) 'or' (c . x)) = TRUE & ( 'not' (a . x)) = TRUE ;

            hence thesis by A3, BINARITH: 10;

          end;

            case

             A7: (( 'not' (b . x)) 'or' (c . x)) = TRUE & (( 'not' (c . x)) 'or' (d . x)) = TRUE ;

            

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

            

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

            now

              per cases by A7, A9, A8, BINARITH: 3;

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

                

                then ((a 'imp' (b 'imp' d)) . x) = (( 'not' (a . x)) 'or' TRUE ) by A3, BINARITH: 10

                .= TRUE by BINARITH: 10;

                hence thesis;

              end;

                case ( 'not' (b . x)) = TRUE & (d . x) = TRUE ;

                hence thesis by A3, BINARITH: 10;

              end;

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

                hence thesis by MARGREL1: 11;

              end;

                case (c . x) = TRUE & (d . x) = TRUE ;

                

                then ((a 'imp' (b 'imp' d)) . x) = (( 'not' (a . x)) 'or' TRUE ) by A3, BINARITH: 10

                .= TRUE by BINARITH: 10;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:31

    for a,b be Function of Y, BOOLEAN holds ((( 'not' a) 'imp' ( 'not' b)) 'imp' (b 'imp' a)) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

        end;

      end;

       A2:

      now

        per cases by XBOOLEAN:def 3;

          case (b . x) = TRUE ;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

        end;

          case (b . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

        end;

      end;

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

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

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

      .= (((( 'not' (b . x)) 'or' (a . x)) 'or' (( 'not' a) . x)) '&' ((( 'not' (b . x)) 'or' (a . x)) 'or' ( 'not' (( 'not' b) . x)))) by XBOOLEAN: 9

      .= ((( 'not' (b . x)) 'or' ((a . x) 'or' (( 'not' a) . x))) '&' ((( 'not' (b . x)) 'or' (a . x)) 'or' ( 'not' (( 'not' b) . x)))) by BINARITH: 11

      .= ((( 'not' (b . x)) 'or' TRUE ) '&' ((( 'not' (b . x)) 'or' (a . x)) 'or' ( 'not' (( 'not' b) . x)))) by A1, MARGREL1:def 19

      .= ( TRUE '&' ((( 'not' (b . x)) 'or' (a . x)) 'or' ( 'not' (( 'not' b) . x)))) by BINARITH: 10

      .= (((a . x) 'or' ( 'not' (b . x))) 'or' ( 'not' (( 'not' b) . x))) by MARGREL1: 14

      .= ((a . x) 'or' (( 'not' (b . x)) 'or' ( 'not' (( 'not' b) . x)))) by BINARITH: 11

      .= ((a . x) 'or' TRUE ) by A2, MARGREL1:def 19

      .= TRUE by BINARITH: 10;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:32

    for a,b be Function of Y, BOOLEAN holds ((a 'imp' b) 'imp' (( 'not' b) 'imp' ( 'not' a))) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

        end;

      end;

       A2:

      now

        per cases by XBOOLEAN:def 3;

          case (b . x) = TRUE ;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

        end;

          case (b . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

        end;

      end;

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

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

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

      .= (((a . x) '&' ( 'not' (b . x))) 'or' (( 'not' ( 'not' (b . x))) 'or' (( 'not' a) . x))) by MARGREL1:def 19

      .= (((b . x) 'or' ( 'not' (a . x))) 'or' ((a . x) '&' ( 'not' (b . x)))) by MARGREL1:def 19

      .= ((((b . x) 'or' ( 'not' (a . x))) 'or' (a . x)) '&' (((b . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x)))) by XBOOLEAN: 9

      .= (((b . x) 'or' TRUE ) '&' (((b . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x)))) by A1, BINARITH: 11

      .= ( TRUE '&' (((b . x) 'or' ( 'not' (a . x))) 'or' ( 'not' (b . x)))) by BINARITH: 10

      .= ((( 'not' (a . x)) 'or' (b . x)) 'or' ( 'not' (b . x))) by MARGREL1: 14

      .= (( 'not' (a . x)) 'or' TRUE ) by A2, BINARITH: 11

      .= TRUE by BINARITH: 10;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:33

    for a,b be Function of Y, BOOLEAN holds ((a 'imp' ( 'not' b)) 'imp' (b 'imp' ( 'not' a))) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

        end;

      end;

       A2:

      now

        per cases by XBOOLEAN:def 3;

          case (b . x) = TRUE ;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

        end;

          case (b . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

        end;

      end;

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

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

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

      .= (((a . x) '&' ( 'not' ( 'not' (b . x)))) 'or' (( 'not' (b . x)) 'or' (( 'not' a) . x))) by MARGREL1:def 19

      .= ((( 'not' (b . x)) 'or' ( 'not' (a . x))) 'or' ((a . x) '&' (b . x))) by MARGREL1:def 19

      .= (((( 'not' (b . x)) 'or' ( 'not' (a . x))) 'or' (a . x)) '&' ((( 'not' (b . x)) 'or' ( 'not' (a . x))) 'or' (b . x))) by XBOOLEAN: 9

      .= ((( 'not' (b . x)) 'or' TRUE ) '&' ((( 'not' (b . x)) 'or' ( 'not' (a . x))) 'or' (b . x))) by A1, BINARITH: 11

      .= ( TRUE '&' ((( 'not' (b . x)) 'or' ( 'not' (a . x))) 'or' (b . x))) by BINARITH: 10

      .= ((( 'not' (a . x)) 'or' ( 'not' (b . x))) 'or' (b . x)) by MARGREL1: 14

      .= (( 'not' (a . x)) 'or' TRUE ) by A2, BINARITH: 11

      .= TRUE by BINARITH: 10;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:34

    for a,b be Function of Y, BOOLEAN holds ((( 'not' a) 'imp' b) 'imp' (( 'not' b) 'imp' a)) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

        end;

      end;

       A2:

      now

        per cases by XBOOLEAN:def 3;

          case (b . x) = TRUE ;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE by BINARITH: 10;

        end;

          case (b . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (b . x)) 'or' (b . x)) = TRUE ;

        end;

      end;

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

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

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

      .= ((( 'not' (a . x)) '&' ( 'not' (b . x))) 'or' (( 'not' (( 'not' b) . x)) 'or' (a . x))) by MARGREL1:def 19

      .= (((b . x) 'or' (a . x)) 'or' (( 'not' (a . x)) '&' ( 'not' (b . x)))) by MARGREL1:def 19

      .= ((((b . x) 'or' (a . x)) 'or' ( 'not' (a . x))) '&' (((b . x) 'or' (a . x)) 'or' ( 'not' (b . x)))) by XBOOLEAN: 9

      .= (((b . x) 'or' TRUE ) '&' (((b . x) 'or' (a . x)) 'or' ( 'not' (b . x)))) by A1, BINARITH: 11

      .= ( TRUE '&' (((b . x) 'or' (a . x)) 'or' ( 'not' (b . x)))) by BINARITH: 10

      .= (((a . x) 'or' (b . x)) 'or' ( 'not' (b . x))) by MARGREL1: 14

      .= ((a . x) 'or' TRUE ) by A2, BINARITH: 11

      .= TRUE by BINARITH: 10;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:35

    for a be Function of Y, BOOLEAN holds ((a 'imp' ( 'not' a)) 'imp' ( 'not' a)) = ( I_el Y)

    proof

      let a be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

        end;

      end;

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

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

      .= (((a . x) '&' ( 'not' ( 'not' (a . x)))) 'or' (( 'not' a) . x)) by MARGREL1:def 19

      .= TRUE by A1, MARGREL1:def 19;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:36

    for a,b be Function of Y, BOOLEAN holds (( 'not' a) 'imp' (a 'imp' b)) = ( I_el Y)

    proof

      let a,b be Function of Y, BOOLEAN ;

      let x be Element of Y;

       A1:

      now

        per cases by XBOOLEAN:def 3;

          case (a . x) = TRUE ;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE by BINARITH: 10;

        end;

          case (a . x) = FALSE ;

          

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

          .= TRUE by BINARITH: 10;

          hence (( 'not' (a . x)) 'or' (a . x)) = TRUE ;

        end;

      end;

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

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

      .= ((a . x) 'or' (( 'not' (a . x)) 'or' (b . x))) by MARGREL1:def 19

      .= ( TRUE 'or' (b . x)) by A1, BINARITH: 11

      .= TRUE by BINARITH: 10;

      hence thesis by BVFUNC_1:def 11;

    end;

    theorem :: BVFUNC_5:37

    for a,b,c be Function of Y, BOOLEAN holds ( 'not' ((a '&' b) '&' c)) = ((( 'not' a) 'or' ( 'not' b)) 'or' ( 'not' c))

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      ( 'not' ((a '&' b) '&' c)) = (( 'not' (a '&' b)) 'or' ( 'not' c)) by BVFUNC_1: 14

      .= ((( 'not' a) 'or' ( 'not' b)) 'or' ( 'not' c)) by BVFUNC_1: 14;

      hence thesis;

    end;

    theorem :: BVFUNC_5:38

    for a,b,c be Function of Y, BOOLEAN holds ( 'not' ((a 'or' b) 'or' c)) = ((( 'not' a) '&' ( 'not' b)) '&' ( 'not' c))

    proof

      let a,b,c be Function of Y, BOOLEAN ;

      ( 'not' ((a 'or' b) 'or' c)) = (( 'not' (a 'or' b)) '&' ( 'not' c)) by BVFUNC_1: 13

      .= ((( 'not' a) '&' ( 'not' b)) '&' ( 'not' c)) by BVFUNC_1: 13;

      hence thesis;

    end;

    theorem :: BVFUNC_5:39

    for a,b,c,d be Function of Y, BOOLEAN holds (a 'or' ((b '&' c) '&' d)) = (((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d))

    proof

      let a,b,c,d be Function of Y, BOOLEAN ;

      (a 'or' ((b '&' c) '&' d)) = ((a 'or' (b '&' c)) '&' (a 'or' d)) by BVFUNC_1: 11

      .= (((a 'or' b) '&' (a 'or' c)) '&' (a 'or' d)) by BVFUNC_1: 11;

      hence thesis;

    end;

    theorem :: BVFUNC_5:40

    for a,b,c,d be Function of Y, BOOLEAN holds (a '&' ((b 'or' c) 'or' d)) = (((a '&' b) 'or' (a '&' c)) 'or' (a '&' d))

    proof

      let a,b,c,d be Function of Y, BOOLEAN ;

      (a '&' ((b 'or' c) 'or' d)) = ((a '&' (b 'or' c)) 'or' (a '&' d)) by BVFUNC_1: 12

      .= (((a '&' b) 'or' (a '&' c)) 'or' (a '&' d)) by BVFUNC_1: 12;

      hence thesis;

    end;