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 Def42;
hence Y is I -satisfied by Def42; :: thesis: verum