take MC-wff ; :: thesis: ( MC-wff is MC-closed & not MC-wff is empty )
thus ( MC-wff is MC-closed & not MC-wff is empty ) ; :: thesis: verum