let P, Q, R be PNPair; :: thesis: ( R in compn Q & rng Q c= union (Subt (rng P)) implies rng R c= union (Subt (rng P)) )
assume that
A1: R in compn Q and
A2: rng Q c= union (Subt (rng P)) ; :: thesis: rng R c= union (Subt (rng P))
consider R1 being PNPair such that
A3: R1 = R and
A4: R1 in comp (untn Q) by A1;
consider z being set such that
A5: R1 in z and
A6: z in { (comp S) where S is PNPair : S in untn Q } by A4, TARSKI:def 4;
consider T being PNPair such that
A7: z = comp T and
A8: T in untn Q by A6;
A9: ex T1 being PNPair st
( T1 = T & rng (T1 `1) = untn (rng (Q `1)) & rng (T1 `2) = untn (rng (Q `2)) ) by A8;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng R or x in union (Subt (rng P)) )
assume A10: x in rng R ; :: thesis: x in union (Subt (rng P))
ex R2 being consistent PNPair st
( R2 = R1 & R2 is_completion_of T ) by A7, A5;
then x in tau (rng T) by A3, A10;
then consider p being Element of LTLB_WFF such that
A11: p in rng T and
A12: x in tau1 . p by LTLAXIO3:def 5;

per cases ( p in untn (rng (Q `1)) or p in untn (rng (Q `2)) ) by XBOOLE_0:def 3, A9, A11;

suppose p in untn (rng (Q `1)) ; :: thesis: x in union (Subt (rng P))

then consider A, B being Element of LTLB_WFF such that
A13: p = untn (A,B) and
A14: A 'U' B in rng (Q `1) ;
set aub = A 'U' B;
rng (Q `1) c= rng Q by XBOOLE_1:7;
then A 'U' B in rng Q by A14;
then consider y being set such that
A15: A 'U' B in y and
A16: y in Subt (rng P) by A2, TARSKI:def 4;
consider q being Element of LTLB_WFF such that
A17: y = Sub . q and
q in rng P by A16;
tau1 . (untn (A,B)) c= (tau1 . (untn (A,B))) \/ ((Sub . A) \/ (Sub . B)) by XBOOLE_1:7;
then tau1 . (untn (A,B)) c= ((tau1 . (untn (A,B))) \/ (Sub . A)) \/ (Sub . B) by XBOOLE_1:4;
then tau1 . (untn (A,B)) c= Sub . (A 'U' B) by LTLAXIO3:def 6;
then x in Sub . q by A17, A15, LTLAXIO3:26, A13, A12;
hence x in union (Subt (rng P)) by A17, A16, TARSKI:def 4; :: thesis: verum

end;

suppose p in untn (rng (Q `2)) ; :: thesis: x in union (Subt (rng P))

then consider A, B being Element of LTLB_WFF such that
A18: p = untn (A,B) and
A19: A 'U' B in rng (Q `2) ;
set aub = A 'U' B;
rng (Q `2) c= rng Q by XBOOLE_1:7;
then A 'U' B in rng Q by A19;
then consider y being set such that
A20: A 'U' B in y and
A21: y in Subt (rng P) by A2, TARSKI:def 4;
consider q being Element of LTLB_WFF such that
A22: y = Sub . q and
q in rng P by A21;
tau1 . (untn (A,B)) c= (tau1 . (untn (A,B))) \/ ((Sub . A) \/ (Sub . B)) by XBOOLE_1:7;
then tau1 . (untn (A,B)) c= ((tau1 . (untn (A,B))) \/ (Sub . A)) \/ (Sub . B) by XBOOLE_1:4;
then tau1 . (untn (A,B)) c= Sub . (A 'U' B) by LTLAXIO3:def 6;
then x in Sub . q by A22, A20, LTLAXIO3:26, A18, A12;
hence x in union (Subt (rng P)) by A22, A21, TARSKI:def 4; :: thesis: verum

end;

end;