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

( p in tau X & q in tau X )

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

assume p 'or' q in tau X ; :: thesis: ( p in tau X & q in tau X )

then ('not' p) '&&' ('not' q) in tau X by Th19;

then ( 'not' p in tau X & 'not' q in tau X ) by Th20;

hence ( p in tau X & q in tau X ) by Th19; :: thesis: verum

( p in tau X & q in tau X )

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

assume p 'or' q in tau X ; :: thesis: ( p in tau X & q in tau X )

then ('not' p) '&&' ('not' q) in tau X by Th19;

then ( 'not' p in tau X & 'not' q in tau X ) by Th20;

hence ( p in tau X & q in tau X ) by Th19; :: thesis: verum