let p, q be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF st untn (p,q) in tau X holds

( p in tau X & q in tau X & p 'U' q in tau X )

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

assume A1: untn (p,q) in tau X ; :: thesis: ( p in tau X & q in tau X & p 'U' q in tau X )

then p '&&' (p 'U' q) in tau X by Th21;

hence ( p in tau X & q in tau X & p 'U' q in tau X ) by A1, Th21, Th20; :: thesis: verum

( p in tau X & q in tau X & p 'U' q in tau X )

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

assume A1: untn (p,q) in tau X ; :: thesis: ( p in tau X & q in tau X & p 'U' q in tau X )

then p '&&' (p 'U' q) in tau X by Th21;

hence ( p in tau X & q in tau X & p 'U' q in tau X ) by A1, Th21, Th20; :: thesis: verum