let Y be Subset of X; :: thesis: Y is I -satisfied
for phi being wff string of S st phi in Y holds
I -TruthEval phi = 1 by DefSat;
hence Y is I -satisfied by DefSat; :: thesis: verum