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