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₁[ 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₁[x,y] )

proof

let x be object ; :: thesis: ( x in LTLB_WFF implies ex y being object st
( y in BOOLEAN & S₁[x,y] ) )
set y = (SAT M) . [n,x];
assume x in LTLB_WFF ; :: thesis: ex y being object st
( y in BOOLEAN & S₁[x,y] )
then reconsider x1 = x as Element of LTLB_WFF ;
take (SAT M) . [n,x] ; :: thesis: ( (SAT M) . [n,x] in BOOLEAN & S₁[x,(SAT M) . [n,x]] )
(SAT M) . [n,x1] in BOOLEAN ;
hence ( (SAT M) . [n,x] in BOOLEAN & S₁[x,(SAT M) . [n,x]] ) ; :: thesis: verum

end;

consider f being Function of LTLB_WFF,BOOLEAN such that
A3: for B being object st B in LTLB_WFF holds
S₁[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