let Y be non empty set ; :: thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))
let a, b, c be Function of Y,BOOLEAN; :: thesis: ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))
for z being Element of Y st (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE holds
(((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
proof
let z be Element of Y; :: thesis: ( (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE implies (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE )
A1: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = (((a 'imp' b) '&' (b 'imp' c)) . z) '&' ((c 'imp' a) . z) by MARGREL1:def 20
.= (((a 'imp' b) . z) '&' ((b 'imp' c) . z)) '&' ((c 'imp' a) . z) by MARGREL1:def 20
.= (((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z)) '&' ((c 'imp' a) . z) by BVFUNC_4:8
.= (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z)) '&' ((c 'imp' a) . z) by BVFUNC_4:8
.= (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z)) '&' ((('not' c) 'or' a) . z) by BVFUNC_4:8
.= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z)) '&' ((('not' c) 'or' a) . z) by BVFUNC_1:def 4
.= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) 'or' a) . z) by BVFUNC_1:def 4
.= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by BVFUNC_1:def 4
.= ((('not' (a . z)) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by MARGREL1:def 19
.= ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by MARGREL1:def 19
.= ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' (('not' (c . z)) 'or' (a . z)) by MARGREL1:def 19 ;
assume A2: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ; :: thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
now :: thesis: ( (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z <> TRUE implies (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE )
A3: ( (('not' (a . z)) '&' ('not' (b . z))) '&' ('not' (c . z)) = TRUE or (('not' (a . z)) '&' ('not' (b . z))) '&' ('not' (c . z)) = FALSE ) by XBOOLEAN:def 3;
assume A4: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z <> TRUE ; :: thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
A5: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = (((a '&' b) '&' c) . z) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by BVFUNC_1:def 4
.= (((a '&' b) . z) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by MARGREL1:def 20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by MARGREL1:def 20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) . z) '&' (('not' c) . z)) by MARGREL1:def 20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) . z) '&' (('not' b) . z)) '&' (('not' c) . z)) by MARGREL1:def 20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' (('not' b) . z)) '&' (('not' c) . z)) by MARGREL1:def 19
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' ('not' (b . z))) '&' (('not' c) . z)) by MARGREL1:def 19
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' ('not' (b . z))) '&' ('not' (c . z))) by MARGREL1:def 19 ;
A6: ( ((a . z) '&' (b . z)) '&' (c . z) = TRUE or ((a . z) '&' (b . z)) '&' (c . z) = FALSE ) by XBOOLEAN:def 3;
now :: thesis: ( ( (a . z) '&' (b . z) = FALSE & (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ) or ( c . z = FALSE & (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ) )
per cases ( (a . z) '&' (b . z) = FALSE or c . z = FALSE ) by A4, A5, A6, MARGREL1:12;
case A7: (a . z) '&' (b . z) = FALSE ; :: thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
now :: thesis: ( ( a . z = FALSE & (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ) or ( b . z = FALSE & (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ) )
per cases ( a . z = FALSE or b . z = FALSE ) by A7, MARGREL1:12;
case A8: a . z = FALSE ; :: thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
now :: thesis: ( ( 'not' (b . z) = FALSE & (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ) or ( 'not' (c . z) = FALSE & (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ) )
per cases ( 'not' (b . z) = FALSE or 'not' (c . z) = FALSE ) by A4, A5, A3, A8, MARGREL1:12;
case 'not' (b . z) = FALSE ; :: thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A8, XBOOLEAN:138; :: thesis: verum
end;
case 'not' (c . z) = FALSE ; :: thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A8; :: thesis: verum
end;
end;
end;
hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; :: thesis: verum
end;
case A9: b . z = FALSE ; :: thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
now :: thesis: ( ( 'not' (a . z) = FALSE & (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ) or ( 'not' (c . z) = FALSE & (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ) )
per cases ( 'not' (a . z) = FALSE or 'not' (c . z) = FALSE ) by A4, A5, A3, A9, MARGREL1:12;
case 'not' (a . z) = FALSE ; :: thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A9; :: thesis: verum
end;
case 'not' (c . z) = FALSE ; :: thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A9, XBOOLEAN:138; :: thesis: verum
end;
end;
end;
hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; :: thesis: verum
end;
end;
end;
hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; :: thesis: verum
end;
case A10: c . z = FALSE ; :: thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
now :: thesis: ( ( 'not' (a . z) = FALSE & (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ) or ( 'not' (b . z) = FALSE & (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ) )
per cases ( 'not' (a . z) = FALSE or 'not' (b . z) = FALSE ) by A4, A5, A3, A10, MARGREL1:12;
case 'not' (a . z) = FALSE ; :: thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A10, XBOOLEAN:138; :: thesis: verum
end;
case 'not' (b . z) = FALSE ; :: thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A10; :: thesis: verum
end;
end;
end;
hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; :: thesis: verum
end;
end;
end;
hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; :: thesis: verum
end;
hence (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; :: thesis: verum
end;
then A11: ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) '<' ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c)) ;
for z being Element of Y st (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE holds
(((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
proof
let z be Element of Y; :: thesis: ( (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE implies (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE )
A12: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = (((a '&' b) '&' c) . z) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by BVFUNC_1:def 4
.= (((a '&' b) . z) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by MARGREL1:def 20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by MARGREL1:def 20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) . z) '&' (('not' c) . z)) by MARGREL1:def 20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) . z) '&' (('not' b) . z)) '&' (('not' c) . z)) by MARGREL1:def 20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' (('not' b) . z)) '&' (('not' c) . z)) by MARGREL1:def 19
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' ('not' (b . z))) '&' (('not' c) . z)) by MARGREL1:def 19
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' ('not' (b . z))) '&' ('not' (c . z))) by MARGREL1:def 19 ;
assume A13: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; :: thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
now :: thesis: ( (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z <> TRUE implies (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE )
A14: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = (((a 'imp' b) '&' (b 'imp' c)) . z) '&' ((c 'imp' a) . z) by MARGREL1:def 20
.= (((a 'imp' b) . z) '&' ((b 'imp' c) . z)) '&' ((c 'imp' a) . z) by MARGREL1:def 20
.= (((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z)) '&' ((c 'imp' a) . z) by BVFUNC_4:8
.= (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z)) '&' ((c 'imp' a) . z) by BVFUNC_4:8
.= (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z)) '&' ((('not' c) 'or' a) . z) by BVFUNC_4:8
.= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z)) '&' ((('not' c) 'or' a) . z) by BVFUNC_1:def 4
.= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) 'or' a) . z) by BVFUNC_1:def 4
.= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by BVFUNC_1:def 4
.= ((('not' (a . z)) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by MARGREL1:def 19
.= ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by MARGREL1:def 19
.= ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' (('not' (c . z)) 'or' (a . z)) by MARGREL1:def 19 ;
assume (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z <> TRUE ; :: thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
then A15: ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' (('not' (c . z)) 'or' (a . z)) = FALSE by A14, XBOOLEAN:def 3;
now :: thesis: ( ( (('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z)) = FALSE & (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ) or ( ('not' (c . z)) 'or' (a . z) = FALSE & (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ) )
per cases ( (('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z)) = FALSE or ('not' (c . z)) 'or' (a . z) = FALSE ) by A15, MARGREL1:12;
case A16: (('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z)) = FALSE ; :: thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
now :: thesis: ( ( ('not' (a . z)) 'or' (b . z) = FALSE & (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ) or ( ('not' (b . z)) 'or' (c . z) = FALSE & (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ) )
per cases ( ('not' (a . z)) 'or' (b . z) = FALSE or ('not' (b . z)) 'or' (c . z) = FALSE ) by A16, MARGREL1:12;
case A17: ('not' (a . z)) 'or' (b . z) = FALSE ; :: thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def 3;
hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE by A13, A12, A17; :: thesis: verum
end;
case A18: ('not' (b . z)) 'or' (c . z) = FALSE ; :: thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
( c . z = TRUE or c . z = FALSE ) by XBOOLEAN:def 3;
hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE by A13, A12, A18; :: thesis: verum
end;
end;
end;
hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ; :: thesis: verum
end;
case A19: ('not' (c . z)) 'or' (a . z) = FALSE ; :: thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def 3;
hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE by A13, A12, A19; :: thesis: verum
end;
end;
end;
hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ; :: thesis: verum
end;
hence (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ; :: thesis: verum
end;
then ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c)) '<' ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) ;
hence ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c)) by A11, BVFUNC_1:15; :: thesis: verum