let X be Subset of MC-wff; :: thesis: for p being Element of MC-wff st p in X holds
X |-_IPC p
let p be Element of MC-wff ; :: thesis: ( p in X implies X |-_IPC p )
assume p in X ; :: thesis: X |-_IPC p
then A2: {p} c= X by ZFMISC_1:31;
{p} |-_IPC p by Th65;
hence X |-_IPC p by A2, Th66; :: thesis: verum