let Y be non empty set ; :: thesis: for a, b, c being Element of Funcs (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 Element of Funcs (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 7
.= (((a '&' b) . z) 'or' ((b '&' c) . z)) 'or' ((c '&' a) . z) by BVFUNC_1:def 7
.= (((a . z) '&' (b . z)) 'or' ((b '&' c) . z)) 'or' ((c '&' a) . z) by MARGREL1:def 21
.= (((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z))) 'or' ((c '&' a) . z) by MARGREL1:def 21
.= (((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z))) 'or' ((c . z) '&' (a . z)) by MARGREL1:def 21 ;
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

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 21
.= (((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z) by MARGREL1:def 21
.= (((a . z) 'or' (b . z)) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z) by BVFUNC_1:def 7
.= (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c 'or' a) . z) by BVFUNC_1:def 7
.= (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z)) by BVFUNC_1:def 7 ;
assume (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z <> TRUE ; :: thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE
then A4: (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z)) = FALSE by A3, XBOOLEAN:def 3;

now

per cases ( ((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z)) = FALSE or (c . z) 'or' (a . z) = FALSE ) by A4, MARGREL1:45;

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

per cases ( (a . z) 'or' (b . z) = FALSE or (b . z) 'or' (c . z) = FALSE ) by A5, MARGREL1:45;

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) by BVFUNC_1:def 15;
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 21
.= (((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z) by MARGREL1:def 21
.= (((a . z) 'or' (b . z)) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z) by BVFUNC_1:def 7
.= (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c 'or' a) . z) by BVFUNC_1:def 7
.= (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z)) by BVFUNC_1:def 7 ;
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

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 . z) '&' (b . z)) 'or' ((b . z) '&' (c . z)) = TRUE or ((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z)) = FALSE ) by XBOOLEAN:def 3;
A15: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = (((a '&' b) 'or' (b '&' c)) . z) 'or' ((c '&' a) . z) by BVFUNC_1:def 7
.= (((a '&' b) . z) 'or' ((b '&' c) . z)) 'or' ((c '&' a) . z) by BVFUNC_1:def 7
.= (((a . z) '&' (b . z)) 'or' ((b '&' c) . z)) 'or' ((c '&' a) . z) by MARGREL1:def 21
.= (((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z))) 'or' ((c '&' a) . z) by MARGREL1:def 21
.= (((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z))) 'or' ((c . z) '&' (a . z)) by MARGREL1:def 21 ;
assume A16: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z <> TRUE ; :: thesis: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE

now

per cases ( ( a . z = FALSE & b . z = FALSE ) or ( b . z = FALSE & c . z = FALSE ) or ( c . z = FALSE & a . z = FALSE ) ) by A16, A15, A14, A13, A12, MARGREL1:45;

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) by BVFUNC_1:def 15;
hence ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) = ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a) by A9, BVFUNC_1:18; :: thesis: verum