defpred S_{1}[ Element of LTLB_WFF , Element of LTLB_WFF , set , set , set ] means ( ( $3 is Element of BOOLEAN & $4 is Element of BOOLEAN implies ex a, b, c being Element of BOOLEAN st

( a = $3 & b = $4 & c = $5 & c = a => b ) ) & ( ( not $3 is Element of BOOLEAN or not $4 is Element of BOOLEAN ) implies $5 = {} ) );

defpred S_{2}[ Element of LTLB_WFF , Element of LTLB_WFF , set , set , set ] means $5 = f . ($1 'U' $2);

deffunc H_{1}( Element of NAT ) -> Element of BOOLEAN = f . (prop $1);

A1: for A, B being Element of LTLB_WFF

for x, y being set ex z being set st S_{1}[A,B,x,y,z]

for a, b, c, d being set st S_{2}[p,q,a,b,c] & S_{2}[p,q,a,b,d] holds

c = d ;

A9: for p, q being Element of LTLB_WFF

for a, b, c, d being set st S_{1}[p,q,a,b,c] & S_{1}[p,q,a,b,d] holds

c = d ;

A10: for A, B being Element of LTLB_WFF

for x, y being set ex z being set st S_{2}[A,B,x,y,z]
;

consider val being ManySortedSet of LTLB_WFF such that

A11: ( val . TFALSUM = 0 & ( for n being Element of NAT holds val . (prop n) = H_{1}(n) ) & ( for p, q being Element of LTLB_WFF holds

( S_{2}[p,q,val . p,val . q,val . (p 'U' q)] & S_{1}[p,q,val . p,val . q,val . (p => q)] ) ) )
from HILBERT2:sch 3(A10, A1, A8, A9);

then reconsider val = val as Function of LTLB_WFF,BOOLEAN by A12, FUNCT_2:3;

take val ; :: thesis: for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( val . TFALSUM = 0 & val . (prop n) = f . (prop n) & val . (A => B) = (val . A) => (val . B) & val . (A 'U' B) = f . (A 'U' B) )

for n being Element of NAT holds

( val . TFALSUM = 0 & val . (prop n) = f . (prop n) & val . (A => B) = (val . A) => (val . B) & val . (A 'U' B) = f . (A 'U' B) ) by A11; :: thesis: verum

( a = $3 & b = $4 & c = $5 & c = a => b ) ) & ( ( not $3 is Element of BOOLEAN or not $4 is Element of BOOLEAN ) implies $5 = {} ) );

defpred S

deffunc H

A1: for A, B being Element of LTLB_WFF

for x, y being set ex z being set st S

proof

A8:
for p, q being Element of LTLB_WFF
let A, B be Element of LTLB_WFF ; :: thesis: for x, y being set ex z being set st S_{1}[A,B,x,y,z]

let x, y be set ; :: thesis: ex z being set st S_{1}[A,B,x,y,z]

end;let x, y be set ; :: thesis: ex z being set st S

per cases
( ( x is Element of BOOLEAN & y is Element of BOOLEAN ) or not x is Element of BOOLEAN or not y is Element of BOOLEAN )
;

end;

suppose that A2:
x is Element of BOOLEAN
and

A3: y is Element of BOOLEAN ; :: thesis: ex z being set st S_{1}[A,B,x,y,z]

A3: y is Element of BOOLEAN ; :: thesis: ex z being set st S

reconsider b = y as Element of BOOLEAN by A3;

reconsider a = x as Element of BOOLEAN by A2;

end;reconsider a = x as Element of BOOLEAN by A2;

per cases
( a = 0 or a = 1 )
by XBOOLEAN:def 3;

end;

suppose A5:
a = 1
; :: thesis: ex z being set st S_{1}[A,B,x,y,z]

end;

suppose
( not x is Element of BOOLEAN or not y is Element of BOOLEAN )
; :: thesis: ex z being set st S_{1}[A,B,x,y,z]

end;

end;

for a, b, c, d being set st S

c = d ;

A9: for p, q being Element of LTLB_WFF

for a, b, c, d being set st S

c = d ;

A10: for A, B being Element of LTLB_WFF

for x, y being set ex z being set st S

consider val being ManySortedSet of LTLB_WFF such that

A11: ( val . TFALSUM = 0 & ( for n being Element of NAT holds val . (prop n) = H

( S

A12: now :: thesis: for x being object st x in LTLB_WFF holds

val . x in BOOLEAN_{1} in BOOLEAN )

assume x in LTLB_WFF ; :: thesis: val . b_{1} in BOOLEAN

then reconsider x1 = x as Element of LTLB_WFF ;

end;

dom val = LTLB_WFF
by PARTFUN1:def 2;val . x in BOOLEAN

A13: now :: thesis: for A, B being Element of LTLB_WFF holds val . (A => B) in BOOLEAN

let x be object ; :: thesis: ( x in LTLB_WFF implies val . blet A, B be Element of LTLB_WFF ; :: thesis: val . (b_{1} => b_{2}) in BOOLEAN

end;per cases
( ( val . A is Element of BOOLEAN & val . B is Element of BOOLEAN ) or not val . A is Element of BOOLEAN or not val . B is Element of BOOLEAN )
;

end;

suppose
( val . A is Element of BOOLEAN & val . B is Element of BOOLEAN )
; :: thesis: val . (b_{1} => b_{2}) in BOOLEAN

then consider a, b, c being Element of BOOLEAN such that

a = val . A and

b = val . B and

A14: c = val . (A => B) and

c = a => b by A11;

thus val . (A => B) in BOOLEAN by A14; :: thesis: verum

end;a = val . A and

b = val . B and

A14: c = val . (A => B) and

c = a => b by A11;

thus val . (A => B) in BOOLEAN by A14; :: thesis: verum

assume x in LTLB_WFF ; :: thesis: val . b

then reconsider x1 = x as Element of LTLB_WFF ;

A15: now :: thesis: for n being Element of NAT holds val . (prop n) in BOOLEAN

let n be Element of NAT ; :: thesis: val . (prop n) in BOOLEAN

val . (prop n) = f . (prop n) by A11;

hence val . (prop n) in BOOLEAN ; :: thesis: verum

end;val . (prop n) = f . (prop n) by A11;

hence val . (prop n) in BOOLEAN ; :: thesis: verum

A16: now :: thesis: for A, B being Element of LTLB_WFF holds val . (A 'U' B) in BOOLEAN

let A, B be Element of LTLB_WFF ; :: thesis: val . (A 'U' B) in BOOLEAN

val . (A 'U' B) = f . (A 'U' B) by A11;

hence val . (A 'U' B) in BOOLEAN ; :: thesis: verum

end;val . (A 'U' B) = f . (A 'U' B) by A11;

hence val . (A 'U' B) in BOOLEAN ; :: thesis: verum

per cases
( x1 = TFALSUM or ex n being Element of NAT st x1 = prop n or ex p, q being Element of LTLB_WFF st x1 = p 'U' q or ex p, q being Element of LTLB_WFF st x1 = p => q )
by Th4;

end;

then reconsider val = val as Function of LTLB_WFF,BOOLEAN by A12, FUNCT_2:3;

take val ; :: thesis: for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( val . TFALSUM = 0 & val . (prop n) = f . (prop n) & val . (A => B) = (val . A) => (val . B) & val . (A 'U' B) = f . (A 'U' B) )

now :: thesis: for A, B being Element of LTLB_WFF holds val . (A => B) = (val . A) => (val . B)

hence
for A, B being Element of LTLB_WFF let A, B be Element of LTLB_WFF ; :: thesis: val . (A => B) = (val . A) => (val . B)

S_{1}[A,B,val . A,val . B,val . (A => B)]
by A11;

hence val . (A => B) = (val . A) => (val . B) ; :: thesis: verum

end;S

hence val . (A => B) = (val . A) => (val . B) ; :: thesis: verum

for n being Element of NAT holds

( val . TFALSUM = 0 & val . (prop n) = f . (prop n) & val . (A => B) = (val . A) => (val . B) & val . (A 'U' B) = f . (A 'U' B) ) by A11; :: thesis: verum