Theorem bex_def

Modification history