a:Assignment, f:Formula, a':Assignment.
a' extends a 
(a |= f a' |= f ) & (a |
f a' | f)
assignment_monotone
a = a
Thm* a:Assignment, f:Formula, a':Assignment.
a' extends a (a |= f a' |= f ) & (a | f a' | f)
assignment_monotone
In prior sections: assignment