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 ) )
assume p '&&' q in tau X ; :: thesis: ( p in tau X & q in tau X )
then A1: p => (q => TFALSUM) in tau X by Th19;
then 'not' q in tau X by Th19;
hence ( p in tau X & q in tau X ) by A1, Th19; :: thesis: verum