let A, B be Element of PL-WFF ; :: thesis: for F being Subset of PL-WFF st F |- A => B holds
F \/ {A} |- B
let F be Subset of PL-WFF; :: thesis: ( F |- A => B implies F \/ {A} |- B )
A in {A} by TARSKI:def 1;
then A in F \/ {A} by XBOOLE_0:def 3;
then A1: F \/ {A} |- A by th42;
assume F |- A => B ; :: thesis: F \/ {A} |- B
then F \/ {A} |- A => B by monmp, XBOOLE_1:7;
hence F \/ {A} |- B by A1, th43; :: thesis: verum