let A, B be Element of LTLB_WFF ; :: thesis: for P being consistent complete PNPair
for Q being Element of compn P st A 'U' B in rng (P `2) holds
( B in rng (Q `2) & ( A in rng (Q `2) or A 'U' B in rng (Q `2) ) )
let P be consistent complete PNPair; :: thesis: for Q being Element of compn P st A 'U' B in rng (P `2) holds
( B in rng (Q `2) & ( A in rng (Q `2) or A 'U' B in rng (Q `2) ) )
let Q be Element of compn P; :: thesis: ( A 'U' B in rng (P `2) implies ( B in rng (Q `2) & ( A in rng (Q `2) or A 'U' B in rng (Q `2) ) ) )
set aub = A 'U' B;
set nb = 'not' B;
set na = 'not' A;
set au = A '&&' (A 'U' B);
('not' (untn (A,B))) => (('not' B) '&&' ('not' (A '&&' (A 'U' B)))) is ctaut by LTLAXIO2:36;
then ('not' (untn (A,B))) => (('not' B) '&&' ('not' (A '&&' (A 'U' B)))) in LTL_axioms by LTLAXIO1:def 17;
then A1: {} LTLB_WFF |- ('not' (untn (A,B))) => (('not' B) '&&' ('not' (A '&&' (A 'U' B)))) by LTLAXIO1:42;
assume A 'U' B in rng (P `2) ; :: thesis: ( B in rng (Q `2) & ( A in rng (Q `2) or A 'U' B in rng (Q `2) ) )
then A2: untn (A,B) in rng (Q `2) by Th21;
then A3: untn (A,B) in rng Q by XBOOLE_0:def 3;
then A4: A in rng Q by Th8;
{} LTLB_WFF |- (Q ^) => ('not' (untn (A,B))) by LTLAXIO3:29, A2;
then A5: {} LTLB_WFF |- (Q ^) => (('not' B) '&&' ('not' (A '&&' (A 'U' B)))) by A1, LTLAXIO1:47;
(('not' B) '&&' ('not' (A '&&' (A 'U' B)))) => ('not' B) is ctaut by LTLAXIO2:27;
then (('not' B) '&&' ('not' (A '&&' (A 'U' B)))) => ('not' B) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- (('not' B) '&&' ('not' (A '&&' (A 'U' B)))) => ('not' B) by LTLAXIO1:42;
then A6: {} LTLB_WFF |- (Q ^) => ('not' B) by LTLAXIO1:47, A5;
(('not' B) '&&' ('not' (A '&&' (A 'U' B)))) => ('not' (A '&&' (A 'U' B))) is ctaut by LTLAXIO2:28;
then (('not' B) '&&' ('not' (A '&&' (A 'U' B)))) => ('not' (A '&&' (A 'U' B))) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- (('not' B) '&&' ('not' (A '&&' (A 'U' B)))) => ('not' (A '&&' (A 'U' B))) by LTLAXIO1:42;
then A7: {} LTLB_WFF |- (Q ^) => ('not' (A '&&' (A 'U' B))) by LTLAXIO1:47, A5;
A8: B in rng Q by A3, Th8;
A9: A 'U' B in rng Q by A3, Th8;
assume A10: ( not B in rng (Q `2) or ( not A in rng (Q `2) & not A 'U' B in rng (Q `2) ) ) ; :: thesis: contradiction

per cases ( not B in rng (Q `2) or ( not A in rng (Q `2) & not A 'U' B in rng (Q `2) ) ) by A10;

suppose not B in rng (Q `2) ; :: thesis: contradiction

then B in rng (Q `1) by A8, XBOOLE_0:def 3;
then {} LTLB_WFF |- (Q ^) => B by LTLAXIO3:28;
then {} LTLB_WFF |- (Q ^) => (B '&&' ('not' B)) by LTLAXIO2:52, A6;
then {} LTLB_WFF |- 'not' (Q ^) by LTLAXIO2:55;
hence contradiction by LTLAXIO3:def 10; :: thesis: verum

end;

suppose A11: ( not A in rng (Q `2) & not A 'U' B in rng (Q `2) ) ; :: thesis: contradiction

then A in rng (Q `1) by XBOOLE_0:def 3, A4;
then A12: {} LTLB_WFF |- (Q ^) => A by LTLAXIO3:28;
A 'U' B in rng (Q `1) by A11, XBOOLE_0:def 3, A9;
then {} LTLB_WFF |- (Q ^) => (A 'U' B) by LTLAXIO3:28;
then {} LTLB_WFF |- (Q ^) => (A '&&' (A 'U' B)) by A12, LTLAXIO2:52;
then {} LTLB_WFF |- (Q ^) => ((A '&&' (A 'U' B)) '&&' ('not' (A '&&' (A 'U' B)))) by LTLAXIO2:52, A7;
then {} LTLB_WFF |- 'not' (Q ^) by LTLAXIO2:55;
hence contradiction by LTLAXIO3:def 10; :: thesis: verum

end;

end;