let p, q be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF st p => q in tau X holds

( p in tau X & q in tau X )

let X be Subset of LTLB_WFF; :: thesis: ( p => q in tau X implies ( p in tau X & q in tau X ) )

set t = { (tau1 . r) where r is Element of LTLB_WFF : r in X } ;

assume p => q in tau X ; :: thesis: ( p in tau X & q in tau X )

then consider B being Element of LTLB_WFF such that

A1: B in X and

A2: p => q in tau1 . B by Def5;

A3: tau1 . B in { (tau1 . r) where r is Element of LTLB_WFF : r in X } by A1;

p in tau1 . B by Th7, A2;

then A4: p in union { (tau1 . r) where r is Element of LTLB_WFF : r in X } by A3, TARSKI:def 4;

q in tau1 . B by Th7, A2;

then q in union { (tau1 . r) where r is Element of LTLB_WFF : r in X } by TARSKI:def 4, A3;

hence ( p in tau X & q in tau X ) by A4, Th15; :: thesis: verum

( p in tau X & q in tau X )

let X be Subset of LTLB_WFF; :: thesis: ( p => q in tau X implies ( p in tau X & q in tau X ) )

set t = { (tau1 . r) where r is Element of LTLB_WFF : r in X } ;

assume p => q in tau X ; :: thesis: ( p in tau X & q in tau X )

then consider B being Element of LTLB_WFF such that

A1: B in X and

A2: p => q in tau1 . B by Def5;

A3: tau1 . B in { (tau1 . r) where r is Element of LTLB_WFF : r in X } by A1;

p in tau1 . B by Th7, A2;

then A4: p in union { (tau1 . r) where r is Element of LTLB_WFF : r in X } by A3, TARSKI:def 4;

q in tau1 . B by Th7, A2;

then q in union { (tau1 . r) where r is Element of LTLB_WFF : r in X } by TARSKI:def 4, A3;

hence ( p in tau X & q in tau X ) by A4, Th15; :: thesis: verum