let u, w, z be Element of BOOLEAN ; :: thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
per cases ( ( z = TRUE & w = TRUE ) or ( w = FALSE & u = TRUE ) or u = FALSE or z = FALSE ) by XBOOLEAN:def 3;
suppose ( z = TRUE & w = TRUE ) ; :: thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
then 'not' (w '&' z) = FALSE by MARGREL1:11;
then ('not' (w '&' z)) '&' (u '&' z) = FALSE by MARGREL1:12;
then ('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1:12;
hence 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE by MARGREL1:11; :: thesis: verum
end;
suppose that A1: w = FALSE and
A2: u = TRUE ; :: thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
'not' w = TRUE by A1, MARGREL1:11;
then 'not' (u '&' ('not' w)) = FALSE by A2, MARGREL1:11;
then ('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1:12;
hence 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE by MARGREL1:11; :: thesis: verum
end;
suppose u = FALSE ; :: thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
then u '&' z = FALSE by MARGREL1:12;
then ('not' (w '&' z)) '&' (u '&' z) = FALSE by MARGREL1:12;
then ('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1:12;
hence 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE by MARGREL1:11; :: thesis: verum
end;
suppose z = FALSE ; :: thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
then u '&' z = FALSE by MARGREL1:12;
then ('not' (w '&' z)) '&' (u '&' z) = FALSE by MARGREL1:12;
then ('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1:12;
hence 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE by MARGREL1:11; :: thesis: verum
end;
end;