now

let phi be wff string of S; :: thesis: ( phi in X \/ Y implies I -TruthEval phi = 1 )
assume phi in X \/ Y ; :: thesis: I -TruthEval phi = 1
then ( phi in X or phi in Y ) by XBOOLE_0:def 3;
hence I -TruthEval phi = 1 by DefSat; :: thesis: verum

end;

hence X \/ Y is I -satisfied by DefSat; :: thesis: verum