let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st A is LTL_TAUT_OF_PL holds

F |= A

let F be Subset of LTLB_WFF; :: thesis: ( A is LTL_TAUT_OF_PL implies F |= A )

assume A1: A is LTL_TAUT_OF_PL ; :: thesis: F |= A

let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( M |= F implies M |= A )

assume M |= F ; :: thesis: M |= A

let n be Element of NAT ; :: according to LTLAXIO1:def 12 :: thesis: (SAT M) . [n,A] = 1

defpred S_{1}[ object , object ] means $2 = (SAT M) . [n,$1];

A2: for x being object st x in LTLB_WFF holds

ex y being object st

( y in BOOLEAN & S_{1}[x,y] )

A3: for B being object st B in LTLB_WFF holds

S_{1}[B,f . B]
from FUNCT_2:sch 1(A2);

thus (SAT M) . [n,A] = (VAL f) . A by A3, Th32

.= 1 by A1 ; :: thesis: verum

F |= A

let F be Subset of LTLB_WFF; :: thesis: ( A is LTL_TAUT_OF_PL implies F |= A )

assume A1: A is LTL_TAUT_OF_PL ; :: thesis: F |= A

let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( M |= F implies M |= A )

assume M |= F ; :: thesis: M |= A

let n be Element of NAT ; :: according to LTLAXIO1:def 12 :: thesis: (SAT M) . [n,A] = 1

defpred S

A2: for x being object st x in LTLB_WFF holds

ex y being object st

( y in BOOLEAN & S

proof

consider f being Function of LTLB_WFF,BOOLEAN such that
let x be object ; :: thesis: ( x in LTLB_WFF implies ex y being object st

( y in BOOLEAN & S_{1}[x,y] ) )

set y = (SAT M) . [n,x];

assume x in LTLB_WFF ; :: thesis: ex y being object st

( y in BOOLEAN & S_{1}[x,y] )

then reconsider x1 = x as Element of LTLB_WFF ;

take (SAT M) . [n,x] ; :: thesis: ( (SAT M) . [n,x] in BOOLEAN & S_{1}[x,(SAT M) . [n,x]] )

(SAT M) . [n,x1] in BOOLEAN ;

hence ( (SAT M) . [n,x] in BOOLEAN & S_{1}[x,(SAT M) . [n,x]] )
; :: thesis: verum

end;( y in BOOLEAN & S

set y = (SAT M) . [n,x];

assume x in LTLB_WFF ; :: thesis: ex y being object st

( y in BOOLEAN & S

then reconsider x1 = x as Element of LTLB_WFF ;

take (SAT M) . [n,x] ; :: thesis: ( (SAT M) . [n,x] in BOOLEAN & S

(SAT M) . [n,x1] in BOOLEAN ;

hence ( (SAT M) . [n,x] in BOOLEAN & S

A3: for B being object st B in LTLB_WFF holds

S

thus (SAT M) . [n,A] = (VAL f) . A by A3, Th32

.= 1 by A1 ; :: thesis: verum