:: BVFUNC10 semantic presentation

theorem :: BVFUNC10:1
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds ((b2 '&' b3) 'or' (b3 '&' b4)) 'or' (b4 '&' b2) = ((b2 'or' b3) '&' (b3 'or' b4)) '&' (b4 'or' b2)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
for b1 being Element of c1 holds
( Pj (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)),b1 = TRUE implies Pj (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)),b1 = TRUE )
proof
let c5 be Element of c1;
assume E1: Pj (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)),c5 = TRUE ;
E2: Pj (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)),c5 = (Pj ((c2 '&' c3) 'or' (c3 '&' c4)),c5) 'or' (Pj (c4 '&' c2),c5) by BVFUNC_1:def 7
.= ((Pj (c2 '&' c3),c5) 'or' (Pj (c3 '&' c4),c5)) 'or' (Pj (c4 '&' c2),c5) by BVFUNC_1:def 7
.= (((Pj c2,c5) '&' (Pj c3,c5)) 'or' (Pj (c3 '&' c4),c5)) 'or' (Pj (c4 '&' c2),c5) by VALUAT_1:def 6
.= (((Pj c2,c5) '&' (Pj c3,c5)) 'or' ((Pj c3,c5) '&' (Pj c4,c5))) 'or' (Pj (c4 '&' c2),c5) by VALUAT_1:def 6
.= (((Pj c2,c5) '&' (Pj c3,c5)) 'or' ((Pj c3,c5) '&' (Pj c4,c5))) 'or' ((Pj c4,c5) '&' (Pj c2,c5)) by VALUAT_1:def 6 ;
now
assume E3: Pj (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)),c5 <> TRUE ;
Pj (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)),c5 = (Pj ((c2 'or' c3) '&' (c3 'or' c4)),c5) '&' (Pj (c4 'or' c2),c5) by VALUAT_1:def 6
.= ((Pj (c2 'or' c3),c5) '&' (Pj (c3 'or' c4),c5)) '&' (Pj (c4 'or' c2),c5) by VALUAT_1:def 6
.= (((Pj c2,c5) 'or' (Pj c3,c5)) '&' (Pj (c3 'or' c4),c5)) '&' (Pj (c4 'or' c2),c5) by BVFUNC_1:def 7
.= (((Pj c2,c5) 'or' (Pj c3,c5)) '&' ((Pj c3,c5) 'or' (Pj c4,c5))) '&' (Pj (c4 'or' c2),c5) by BVFUNC_1:def 7
.= (((Pj c2,c5) 'or' (Pj c3,c5)) '&' ((Pj c3,c5) 'or' (Pj c4,c5))) '&' ((Pj c4,c5) 'or' (Pj c2,c5)) by BVFUNC_1:def 7 ;
then E4: (((Pj c2,c5) 'or' (Pj c3,c5)) '&' ((Pj c3,c5) 'or' (Pj c4,c5))) '&' ((Pj c4,c5) 'or' (Pj c2,c5)) = FALSE by E3, MARGREL1:43;
now
per cases ( ((Pj c2,c5) 'or' (Pj c3,c5)) '&' ((Pj c3,c5) 'or' (Pj c4,c5)) = FALSE or (Pj c4,c5) 'or' (Pj c2,c5) = FALSE ) by E4, MARGREL1:45;
case E5: ((Pj c2,c5) 'or' (Pj c3,c5)) '&' ((Pj c3,c5) 'or' (Pj c4,c5)) = FALSE ;
now
per cases ( (Pj c2,c5) 'or' (Pj c3,c5) = FALSE or (Pj c3,c5) 'or' (Pj c4,c5) = FALSE ) by E5, MARGREL1:45;
case E6: (Pj c2,c5) 'or' (Pj c3,c5) = FALSE ;
E7: ( Pj c2,c5 = TRUE or Pj c2,c5 = FALSE ) by MARGREL1:39;
( Pj c3,c5 = TRUE or Pj c3,c5 = FALSE ) by MARGREL1:39;
then ( Pj c2,c5 = FALSE & Pj c3,c5 = FALSE ) by E6, E7, BINARITH:19;
then (((Pj c2,c5) '&' (Pj c3,c5)) 'or' ((Pj c3,c5) '&' (Pj c4,c5))) 'or' ((Pj c4,c5) '&' (Pj c2,c5)) = (FALSE 'or' (FALSE '&' (Pj c4,c5))) 'or' ((Pj c4,c5) '&' FALSE ) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' (FALSE '&' (Pj c4,c5)) by MARGREL1:49
.= FALSE 'or' (FALSE '&' (Pj c4,c5)) by BINARITH:7
.= FALSE '&' (Pj c4,c5) by BINARITH:7
.= FALSE by MARGREL1:49 ;
hence Pj (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)),c5 = TRUE by E1, E2, MARGREL1:43;
end;
case E6: (Pj c3,c5) 'or' (Pj c4,c5) = FALSE ;
E7: ( Pj c3,c5 = TRUE or Pj c3,c5 = FALSE ) by MARGREL1:39;
( Pj c4,c5 = TRUE or Pj c4,c5 = FALSE ) by MARGREL1:39;
then ( Pj c3,c5 = FALSE & Pj c4,c5 = FALSE ) by E6, E7, BINARITH:19;
then (((Pj c2,c5) '&' (Pj c3,c5)) 'or' ((Pj c3,c5) '&' (Pj c4,c5))) 'or' ((Pj c4,c5) '&' (Pj c2,c5)) = (FALSE 'or' (FALSE '&' FALSE )) 'or' (FALSE '&' (Pj c2,c5)) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' (FALSE '&' (Pj c2,c5)) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' FALSE by MARGREL1:49
.= FALSE 'or' FALSE by BINARITH:7
.= FALSE by BINARITH:7 ;
hence Pj (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)),c5 = TRUE by E1, E2, MARGREL1:43;
end;
end;
end;
hence Pj (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)),c5 = TRUE ;
end;
case E5: (Pj c4,c5) 'or' (Pj c2,c5) = FALSE ;
E6: ( Pj c4,c5 = TRUE or Pj c4,c5 = FALSE ) by MARGREL1:39;
( Pj c2,c5 = TRUE or Pj c2,c5 = FALSE ) by MARGREL1:39;
then ( Pj c4,c5 = FALSE & Pj c2,c5 = FALSE ) by E5, E6, BINARITH:19;
then (((Pj c2,c5) '&' (Pj c3,c5)) 'or' ((Pj c3,c5) '&' (Pj c4,c5))) 'or' ((Pj c4,c5) '&' (Pj c2,c5)) = (FALSE 'or' (FALSE '&' (Pj c3,c5))) 'or' (FALSE '&' FALSE ) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' (FALSE '&' FALSE ) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' FALSE by MARGREL1:49
.= FALSE 'or' FALSE by BINARITH:7
.= FALSE by BINARITH:7 ;
hence Pj (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)),c5 = TRUE by E1, E2, MARGREL1:43;
end;
end;
end;
hence Pj (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)),c5 = TRUE ;
end;
hence Pj (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)),c5 = TRUE ;
end;
then E1: ((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2) '<' ((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2) by BVFUNC_1:def 15;
for b1 being Element of c1 holds
( Pj (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)),b1 = TRUE implies Pj (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)),b1 = TRUE )
proof
let c5 be Element of c1;
assume E2: Pj (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)),c5 = TRUE ;
E3: Pj (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)),c5 = (Pj ((c2 'or' c3) '&' (c3 'or' c4)),c5) '&' (Pj (c4 'or' c2),c5) by VALUAT_1:def 6
.= ((Pj (c2 'or' c3),c5) '&' (Pj (c3 'or' c4),c5)) '&' (Pj (c4 'or' c2),c5) by VALUAT_1:def 6
.= (((Pj c2,c5) 'or' (Pj c3,c5)) '&' (Pj (c3 'or' c4),c5)) '&' (Pj (c4 'or' c2),c5) by BVFUNC_1:def 7
.= (((Pj c2,c5) 'or' (Pj c3,c5)) '&' ((Pj c3,c5) 'or' (Pj c4,c5))) '&' (Pj (c4 'or' c2),c5) by BVFUNC_1:def 7
.= (((Pj c2,c5) 'or' (Pj c3,c5)) '&' ((Pj c3,c5) 'or' (Pj c4,c5))) '&' ((Pj c4,c5) 'or' (Pj c2,c5)) by BVFUNC_1:def 7 ;
now
assume E4: Pj (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)),c5 <> TRUE ;
E5: Pj (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)),c5 = (Pj ((c2 '&' c3) 'or' (c3 '&' c4)),c5) 'or' (Pj (c4 '&' c2),c5) by BVFUNC_1:def 7
.= ((Pj (c2 '&' c3),c5) 'or' (Pj (c3 '&' c4),c5)) 'or' (Pj (c4 '&' c2),c5) by BVFUNC_1:def 7
.= (((Pj c2,c5) '&' (Pj c3,c5)) 'or' (Pj (c3 '&' c4),c5)) 'or' (Pj (c4 '&' c2),c5) by VALUAT_1:def 6
.= (((Pj c2,c5) '&' (Pj c3,c5)) 'or' ((Pj c3,c5) '&' (Pj c4,c5))) 'or' (Pj (c4 '&' c2),c5) by VALUAT_1:def 6
.= (((Pj c2,c5) '&' (Pj c3,c5)) 'or' ((Pj c3,c5) '&' (Pj c4,c5))) 'or' ((Pj c4,c5) '&' (Pj c2,c5)) by VALUAT_1:def 6 ;
E6: ( ((Pj c2,c5) '&' (Pj c3,c5)) 'or' ((Pj c3,c5) '&' (Pj c4,c5)) = TRUE or ((Pj c2,c5) '&' (Pj c3,c5)) 'or' ((Pj c3,c5) '&' (Pj c4,c5)) = FALSE ) by MARGREL1:39;
E7: ( (Pj c4,c5) '&' (Pj c2,c5) = TRUE or (Pj c4,c5) '&' (Pj c2,c5) = FALSE ) by MARGREL1:39;
E8: ( (Pj c2,c5) '&' (Pj c3,c5) = TRUE or (Pj c2,c5) '&' (Pj c3,c5) = FALSE ) by MARGREL1:39;
( (Pj c3,c5) '&' (Pj c4,c5) = TRUE or (Pj c3,c5) '&' (Pj c4,c5) = FALSE ) by MARGREL1:39;
then E9: ( (Pj c2,c5) '&' (Pj c3,c5) = FALSE & (Pj c3,c5) '&' (Pj c4,c5) = FALSE ) by E4, E5, E6, E8, BINARITH:19;
now
per cases not ( not ( Pj c2,c5 = FALSE & Pj c3,c5 = FALSE ) & not ( Pj c3,c5 = FALSE & Pj c4,c5 = FALSE ) & not ( Pj c4,c5 = FALSE & Pj c2,c5 = FALSE ) ) by E4, E5, E7, E9, BINARITH:19, MARGREL1:45;
case ( Pj c2,c5 = FALSE & Pj c3,c5 = FALSE ) ;
then (((Pj c2,c5) 'or' (Pj c3,c5)) '&' ((Pj c3,c5) 'or' (Pj c4,c5))) '&' ((Pj c4,c5) 'or' (Pj c2,c5)) = (FALSE '&' (FALSE 'or' (Pj c4,c5))) '&' ((Pj c4,c5) 'or' FALSE ) by BINARITH:7
.= (FALSE '&' (Pj c4,c5)) '&' ((Pj c4,c5) 'or' FALSE ) by BINARITH:7
.= (FALSE '&' (Pj c4,c5)) '&' (Pj c4,c5) by BINARITH:7
.= FALSE '&' ((Pj c4,c5) '&' (Pj c4,c5)) by MARGREL1:52
.= FALSE by MARGREL1:49 ;
hence Pj (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)),c5 = TRUE by E2, E3, MARGREL1:43;
end;
case ( Pj c3,c5 = FALSE & Pj c4,c5 = FALSE ) ;
then (((Pj c2,c5) 'or' (Pj c3,c5)) '&' ((Pj c3,c5) 'or' (Pj c4,c5))) '&' ((Pj c4,c5) 'or' (Pj c2,c5)) = ((Pj c2,c5) '&' (FALSE 'or' FALSE )) '&' (FALSE 'or' (Pj c2,c5)) by BINARITH:7
.= ((Pj c2,c5) '&' FALSE ) '&' (FALSE 'or' (Pj c2,c5)) by BINARITH:7
.= (FALSE '&' (Pj c2,c5)) '&' (Pj c2,c5) by BINARITH:7
.= FALSE '&' ((Pj c2,c5) '&' (Pj c2,c5)) by MARGREL1:52
.= FALSE by MARGREL1:49 ;
hence Pj (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)),c5 = TRUE by E2, E3, MARGREL1:43;
end;
case ( Pj c4,c5 = FALSE & Pj c2,c5 = FALSE ) ;
then (((Pj c2,c5) 'or' (Pj c3,c5)) '&' ((Pj c3,c5) 'or' (Pj c4,c5))) '&' ((Pj c4,c5) 'or' (Pj c2,c5)) = ((Pj c3,c5) '&' ((Pj c3,c5) 'or' FALSE )) '&' (FALSE 'or' FALSE ) by BINARITH:7
.= ((Pj c3,c5) '&' (Pj c3,c5)) '&' (FALSE 'or' FALSE ) by BINARITH:7
.= FALSE '&' ((Pj c3,c5) '&' (Pj c3,c5)) by BINARITH:7
.= FALSE by MARGREL1:49 ;
hence Pj (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)),c5 = TRUE by E2, E3, MARGREL1:43;
end;
end;
end;
hence Pj (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)),c5 = TRUE ;
end;
hence Pj (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)),c5 = TRUE ;
end;
then ((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2) '<' ((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2) by BVFUNC_1:def 15;
hence ((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2) = ((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2) by E1, BVFUNC_1:18;
end;

E1: for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds ((b2 '&' ('not' b3)) 'or' (b3 '&' ('not' b4))) 'or' (b4 '&' ('not' b2)) '<' ((b3 '&' ('not' b2)) 'or' (b4 '&' ('not' b3))) 'or' (b2 '&' ('not' b4))
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
let c5 be Element of c1; :: uses BVFUNC_1:def 15
assume E2: Pj (((c2 '&' ('not' c3)) 'or' (c3 '&' ('not' c4))) 'or' (c4 '&' ('not' c2))),c5 = TRUE ;
E3: Pj (((c2 '&' ('not' c3)) 'or' (c3 '&' ('not' c4))) 'or' (c4 '&' ('not' c2))),c5 = (Pj ((c2 '&' ('not' c3)) 'or' (c3 '&' ('not' c4))),c5) 'or' (Pj (c4 '&' ('not' c2)),c5) by BVFUNC_1:def 7
.= ((Pj (c2 '&' ('not' c3)),c5) 'or' (Pj (c3 '&' ('not' c4)),c5)) 'or' (Pj (c4 '&' ('not' c2)),c5) by BVFUNC_1:def 7
.= (((Pj c2,c5) '&' (Pj ('not' c3),c5)) 'or' (Pj (c3 '&' ('not' c4)),c5)) 'or' (Pj (c4 '&' ('not' c2)),c5) by VALUAT_1:def 6
.= (((Pj c2,c5) '&' (Pj ('not' c3),c5)) 'or' ((Pj c3,c5) '&' (Pj ('not' c4),c5))) 'or' (Pj (c4 '&' ('not' c2)),c5) by VALUAT_1:def 6
.= (((Pj c2,c5) '&' (Pj ('not' c3),c5)) 'or' ((Pj c3,c5) '&' (Pj ('not' c4),c5))) 'or' ((Pj c4,c5) '&' (Pj ('not' c2),c5)) by VALUAT_1:def 6
.= (((Pj c2,c5) '&' ('not' (Pj c3,c5))) 'or' ((Pj c3,c5) '&' (Pj ('not' c4),c5))) 'or' ((Pj c4,c5) '&' (Pj ('not' c2),c5)) by VALUAT_1:def 5
.= (((Pj c2,c5) '&' ('not' (Pj c3,c5))) 'or' ((Pj c3,c5) '&' ('not' (Pj c4,c5)))) 'or' ((Pj c4,c5) '&' (Pj ('not' c2),c5)) by VALUAT_1:def 5
.= (((Pj c2,c5) '&' ('not' (Pj c3,c5))) 'or' ((Pj c3,c5) '&' ('not' (Pj c4,c5)))) 'or' ((Pj c4,c5) '&' ('not' (Pj c2,c5))) by VALUAT_1:def 5 ;
now
assume E4: Pj (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4))),c5 <> TRUE ;
E5: Pj (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4))),c5 = (Pj ((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))),c5) 'or' (Pj (c2 '&' ('not' c4)),c5) by BVFUNC_1:def 7
.= ((Pj (c3 '&' ('not' c2)),c5) 'or' (Pj (c4 '&' ('not' c3)),c5)) 'or' (Pj (c2 '&' ('not' c4)),c5) by BVFUNC_1:def 7
.= (((Pj c3,c5) '&' (Pj ('not' c2),c5)) 'or' (Pj (c4 '&' ('not' c3)),c5)) 'or' (Pj (c2 '&' ('not' c4)),c5) by VALUAT_1:def 6
.= (((Pj c3,c5) '&' (Pj ('not' c2),c5)) 'or' ((Pj c4,c5) '&' (Pj ('not' c3),c5))) 'or' (Pj (c2 '&' ('not' c4)),c5) by VALUAT_1:def 6
.= (((Pj c3,c5) '&' (Pj ('not' c2),c5)) 'or' ((Pj c4,c5) '&' (Pj ('not' c3),c5))) 'or' ((Pj c2,c5) '&' (Pj ('not' c4),c5)) by VALUAT_1:def 6 ;
E6: ( ((Pj c3,c5) '&' (Pj ('not' c2),c5)) 'or' ((Pj c4,c5) '&' (Pj ('not' c3),c5)) = TRUE or ((Pj c3,c5) '&' (Pj ('not' c2),c5)) 'or' ((Pj c4,c5) '&' (Pj ('not' c3),c5)) = FALSE ) by MARGREL1:39;
E7: ( (Pj c2,c5) '&' (Pj ('not' c4),c5) = TRUE or (Pj c2,c5) '&' (Pj ('not' c4),c5) = FALSE ) by MARGREL1:39;
E8: ( (Pj c3,c5) '&' (Pj ('not' c2),c5) = TRUE or (Pj c3,c5) '&' (Pj ('not' c2),c5) = FALSE ) by MARGREL1:39;
( (Pj c4,c5) '&' (Pj ('not' c3),c5) = TRUE or (Pj c4,c5) '&' (Pj ('not' c3),c5) = FALSE ) by MARGREL1:39;
then E9: ( (Pj c3,c5) '&' (Pj ('not' c2),c5) = FALSE & (Pj c4,c5) '&' (Pj ('not' c3),c5) = FALSE ) by E4, E5, E6, E8, BINARITH:19;
then E10: ( Pj c3,c5 = FALSE or Pj ('not' c2),c5 = FALSE ) by MARGREL1:45;
E11: ( Pj c4,c5 = FALSE or Pj ('not' c3),c5 = FALSE ) by E9, MARGREL1:45;
now
per cases ( Pj c2,c5 = FALSE or Pj ('not' c4),c5 = FALSE ) by E4, E5, E7, BINARITH:19, MARGREL1:45;
case E12: Pj c2,c5 = FALSE ;
then 'not' (Pj c2,c5) = TRUE by MARGREL1:41;
then E13: 'not' (Pj c2,c5) <> FALSE by MARGREL1:43;
then 'not' (Pj c3,c5) = TRUE by E10, MARGREL1:41, VALUAT_1:def 5;
then 'not' (Pj c3,c5) <> FALSE by MARGREL1:43;
then 'not' (Pj c4,c5) = TRUE by E11, MARGREL1:41, VALUAT_1:def 5;
then (((Pj c2,c5) '&' ('not' (Pj c3,c5))) 'or' ((Pj c3,c5) '&' ('not' (Pj c4,c5)))) 'or' ((Pj c4,c5) '&' ('not' (Pj c2,c5))) = (FALSE 'or' (FALSE '&' TRUE )) 'or' (FALSE '&' TRUE ) by E10, E11, E12, E13, MARGREL1:49, VALUAT_1:def 5
.= (FALSE 'or' FALSE ) 'or' (FALSE '&' TRUE ) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' FALSE by MARGREL1:49
.= FALSE 'or' FALSE by BINARITH:7
.= FALSE by BINARITH:7 ;
hence Pj (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4))),c5 = TRUE by E2, E3, MARGREL1:43;
end;
case Pj ('not' c4),c5 = FALSE ;
then E12: 'not' (Pj c4,c5) = FALSE by VALUAT_1:def 5;
then E13: Pj c4,c5 = TRUE by MARGREL1:41;
then 'not' (Pj c3,c5) = FALSE by E11, MARGREL1:43, VALUAT_1:def 5;
then E14: Pj c3,c5 = TRUE by MARGREL1:41;
then 'not' (Pj c2,c5) = FALSE by E10, MARGREL1:43, VALUAT_1:def 5;
then Pj c2,c5 = TRUE by MARGREL1:41;
then (((Pj c2,c5) '&' ('not' (Pj c3,c5))) 'or' ((Pj c3,c5) '&' ('not' (Pj c4,c5)))) 'or' ((Pj c4,c5) '&' ('not' (Pj c2,c5))) = (FALSE 'or' (TRUE '&' FALSE )) 'or' (TRUE '&' FALSE ) by E12, E13, E14, MARGREL1:50
.= (FALSE 'or' FALSE ) 'or' (TRUE '&' FALSE ) by MARGREL1:50
.= (FALSE 'or' FALSE ) 'or' FALSE by MARGREL1:50
.= FALSE 'or' FALSE by BINARITH:7
.= FALSE by BINARITH:7 ;
hence Pj (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4))),c5 = TRUE by E2, E3, MARGREL1:43;
end;
end;
end;
hence Pj (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4))),c5 = TRUE ;
end;
hence Pj (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4))),c5 = TRUE ;
end;

theorem :: BVFUNC10:2
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds ((b2 '&' ('not' b3)) 'or' (b3 '&' ('not' b4))) 'or' (b4 '&' ('not' b2)) = ((b3 '&' ('not' b2)) 'or' (b4 '&' ('not' b3))) 'or' (b2 '&' ('not' b4))
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E2: ((c2 '&' ('not' c3)) 'or' (c3 '&' ('not' c4))) 'or' (c4 '&' ('not' c2)) '<' ((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4)) by E1;
((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4)) '<' ((c2 '&' ('not' c3)) 'or' (c3 '&' ('not' c4))) 'or' (c4 '&' ('not' c2)) by E1;
hence ((c2 '&' ('not' c3)) 'or' (c3 '&' ('not' c4))) 'or' (c4 '&' ('not' c2)) = ((c3 '&' ('not' c2)) 'or' (c4 '&' (