let w be boolean object ; :: thesis: ( ( v = FALSE implies ( w = 'not' v iff w = TRUE ) ) & ( not v = FALSE implies ( w = 'not' v iff w = FALSE ) ) )
thus ( v = FALSE implies ( w = 'not' v iff w = TRUE ) ) ; :: thesis: ( not v = FALSE implies ( w = 'not' v iff w = FALSE ) )
assume v <> FALSE ; :: thesis: ( w = 'not' v iff w = FALSE )
then v = TRUE by XBOOLEAN:def 3;
hence ( w = 'not' v iff w = FALSE ) ; :: thesis: verum