take the I -satisfied Subset of 1 ; :: thesis: the I -satisfied Subset of 1 is I -satisfied
thus the I -satisfied Subset of 1 is I -satisfied ; :: thesis: verum