let A, B be Element of LTLB_WFF ; :: thesis: for P, Q being PNPair st A 'U' B in rng (P `2) & Q in compn P holds
untn (A,B) in rng (Q `2)
let P, Q be PNPair; :: thesis: ( A 'U' B in rng (P `2) & Q in compn P implies untn (A,B) in rng (Q `2) )
assume that
A1: A 'U' B in rng (P `2) and
A2: Q in compn P ; :: thesis: untn (A,B) in rng (Q `2)
consider Q1 being Element of [:(LTLB_WFF **),(LTLB_WFF **):] such that
Q = Q1 and
A3: Q1 in comp (untn P) by A2;
consider x being set such that
Q1 in x and
A4: x in { (comp R) where R is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : R in untn P } by TARSKI:def 4, A3;
consider R being PNPair such that
x = comp R and
A5: R in untn P by A4;
ex R1 being PNPair st
( R1 = R & rng (R1 `1) = untn (rng (P `1)) & rng (R1 `2) = untn (rng (P `2)) ) by A5;
then A6: untn (A,B) in rng (R `2) by A1;
Q is_completion_of R by A5, A2, Th19;
then rng (R `2) c= rng (Q `2) ;
hence untn (A,B) in rng (Q `2) by A6; :: thesis: verum