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

per cases ( not A in rng (Q `1) or not A 'U' B in rng (Q `1) ) by A9;

suppose not A in rng (Q `1) ; :: thesis: contradiction

then A in rng (Q `2) by A3, XBOOLE_0:def 3;
then {} LTLB_WFF |- (Q ^) => ('not' A) by LTLAXIO3:29;
then {} LTLB_WFF |- (Q ^) => (('not' A) '&&' ('not' B)) by LTLAXIO2:52, A10;
hence contradiction by LTLAXIO1:43, A6, LTLAXIO3:def 10; :: thesis: verum

end;

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

then A 'U' B in rng (Q `2) by XBOOLE_0:def 3, A4;
then {} LTLB_WFF |- (Q ^) => ('not' (A 'U' B)) by LTLAXIO3:29;
then {} LTLB_WFF |- (Q ^) => (('not' B) '&&' ('not' (A 'U' B))) by LTLAXIO2:52, A10;
hence contradiction by LTLAXIO1:43, A7, LTLAXIO3:def 10; :: thesis: verum

end;

end;