let A, B be Element of LTLB_WFF ; :: thesis: for P being complete PNPair st untn (A,B) in rng P holds
( A in rng P & B in rng P & A 'U' B in rng P )
let P be complete PNPair; :: thesis: ( untn (A,B) in rng P implies ( A in rng P & B in rng P & A 'U' B in rng P ) )
assume A1: untn (A,B) in rng P ; :: thesis: ( A in rng P & B in rng P & A 'U' B in rng P )
tau (rng P) = rng P by LTLAXIO3:def 11;
hence ( A in rng P & B in rng P & A 'U' B in rng P ) by A1, LTLAXIO3:22; :: thesis: verum