now :: thesis: for phi being wff string of S st phi in X \/ Y holds

I -TruthEval phi = 1

hence
X \/ Y is I -satisfied
; :: thesis: verumI -TruthEval phi = 1

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 Def41; :: thesis: verum

end;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 Def41; :: thesis: verum