let x, y be Element of BOOLEAN ; :: thesis: ( ( not x 'or' y = TRUE or x = TRUE or y = TRUE ) & ( ( x = TRUE or y = TRUE ) implies x 'or' y = TRUE ) & ( x 'or' y = FALSE implies ( x = FALSE & y = FALSE ) ) & ( x = FALSE & y = FALSE implies x 'or' y = FALSE ) )
thus ( not x 'or' y = TRUE or x = TRUE or y = TRUE ) :: thesis: ( ( ( x = TRUE or y = TRUE ) implies x 'or' y = TRUE ) & ( x 'or' y = FALSE implies ( x = FALSE & y = FALSE ) ) & ( x = FALSE & y = FALSE implies x 'or' y = FALSE ) )

proof

assume x 'or' y = TRUE ; :: thesis: ( x = TRUE or y = TRUE )
then ( 'not' x = FALSE or 'not' y = FALSE ) by MARGREL1:12;
hence ( x = TRUE or y = TRUE ) ; :: thesis: verum

end;

thus ( ( x = TRUE or y = TRUE ) implies x 'or' y = TRUE ) ; :: thesis: ( x 'or' y = FALSE iff ( x = FALSE & y = FALSE ) )
thus ( x 'or' y = FALSE implies ( x = FALSE & y = FALSE ) ) :: thesis: ( x = FALSE & y = FALSE implies x 'or' y = FALSE )

proof

assume A1: x 'or' y = FALSE ; :: thesis: ( x = FALSE & y = FALSE )
then 'not' x = TRUE by MARGREL1:12;
hence ( x = FALSE & y = FALSE ) by A1; :: thesis: verum

end;

thus ( x = FALSE & y = FALSE implies x 'or' y = FALSE ) ; :: thesis: verum