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