let p, q be Element of LTLB_WFF ; :: thesis: ( p in tau1 . q & p <> q implies len p < len q )
defpred S₁[ Element of LTLB_WFF ] means ( p in tau1 . $1 & p <> $1 implies len p < len $1 );
A1: for n being Element of NAT holds S₁[ prop n]

proof

let n be Element of NAT ; :: thesis: S₁[ prop n]
tau1 . (prop n) = {(prop n)} by Def4;
hence S₁[ prop n] by TARSKI:def 1; :: thesis: verum

end;

A2: for r, s being Element of LTLB_WFF st S₁[r] & S₁[s] holds
( S₁[r 'U' s] & S₁[r => s] )

proof

let r, s be Element of LTLB_WFF ; :: thesis: ( S₁[r] & S₁[s] implies ( S₁[r 'U' s] & S₁[r => s] ) )
assume that
A3: S₁[r] and
A4: S₁[s] ; :: thesis: ( S₁[r 'U' s] & S₁[r => s] )
set u = r => s;
tau1 . (r 'U' s) = {(r 'U' s)} by Def4;
hence S₁[r 'U' s] by TARSKI:def 1; :: thesis: S₁[r => s]
thus S₁[r => s] :: thesis: verum

proof

assume that
A5: p in tau1 . (r => s) and
A6: p <> r => s ; :: thesis: len p < len (r => s)
tau1 . (r => s) = ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) by Def4;
then p in {(r => s)} \/ ((tau1 . r) \/ (tau1 . s)) by XBOOLE_1:4, A5;
then A7: ( p in {(r => s)} or p in (tau1 . r) \/ (tau1 . s) ) by XBOOLE_0:def 3;

per cases ( p in tau1 . r or p in tau1 . s ) by A7, TARSKI:def 1, A6, XBOOLE_0:def 3;

suppose p in tau1 . r ; :: thesis: len p < len (r => s)

hence len p < len (r => s) by HILBERT2:16, XXREAL_0:2, A3; :: thesis: verum

end;

suppose p in tau1 . s ; :: thesis: len p < len (r => s)

hence len p < len (r => s) by HILBERT2:16, XXREAL_0:2, A4; :: thesis: verum

end;

end;

end;

end;

tau1 . TFALSUM = {TFALSUM} by Def4;
then A8: S₁[ TFALSUM ] by TARSKI:def 1;
for p being Element of LTLB_WFF holds S₁[p] from HILBERT2:sch 2(A8, A1, A2);
hence ( p in tau1 . q & p <> q implies len p < len q ) ; :: thesis: verum