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

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