let p be Element of MC-wff ; :: thesis: |-_IPC p 'equiv' p
|-_IPC p => p by Th85;
hence |-_IPC p 'equiv' p by Th83; :: thesis: verum