let A, B be Element of PL-WFF ; :: thesis: for F being Subset of PL-WFF st F |= A & F |= A => B holds
F |= B
let F be Subset of PL-WFF; :: thesis: ( F |= A & F |= A => B implies F |= B )
assume that
A1: F |= A and
A2: F |= A => B ; :: thesis: F |= B
let M be PLModel; :: according to PL_AXIOM:def 17 :: thesis: ( M |= F implies M |= B )
assume A3: M |= F ; :: thesis: M |= B
then M |= A => B by A2;
then A4: ((SAT M) . A) => ((SAT M) . B) = 1 by Def11;
M |= A by A1, A3;
hence (SAT M) . B = 1 by A4; :: according to PL_AXIOM:def 15 :: thesis: verum