let P, Q, R be PNPair; ( 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))
; 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 ; TARSKI:def 3 ( not x in rng R or x in union (Subt (rng P)) )
assume A10:
x in rng R
; 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))
;
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;
verum end; suppose
p in untn (rng (Q `2))
;
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;
verum end; end;