let p, q be Element of LTLB_WFF ; :: thesis: p 'U' q in Sub . (p 'U' q)
set puq = p 'U' q;
A1: tau1 . (p 'U' q) c= tau1 . (p '&&' (p 'U' q)) by Th13;
p 'U' q in {(p 'U' q)} by TARSKI:def 1;
then A2: p 'U' q in tau1 . (p 'U' q) by Def4;
(tau1 . (untn (p,q))) \/ (Sub . p) c= ((tau1 . (untn (p,q))) \/ (Sub . p)) \/ (Sub . q) by XBOOLE_1:7;
then ( tau1 . (untn (p,q)) c= (tau1 . (untn (p,q))) \/ (Sub . p) & (tau1 . (untn (p,q))) \/ (Sub . p) c= Sub . (p 'U' q) ) by XBOOLE_1:7, Def6;
then A3: tau1 . (untn (p,q)) c= Sub . (p 'U' q) ;
tau1 . (p '&&' (p 'U' q)) c= tau1 . (untn (p,q)) by Th14;
then tau1 . (p '&&' (p 'U' q)) c= Sub . (p 'U' q) by A3;
then tau1 . (p 'U' q) c= Sub . (p 'U' q) by A1;
hence p 'U' q in Sub . (p 'U' q) by A2; :: thesis: verum