let S be non empty set ; :: thesis: for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for a being Assign of (CTLModel R,BASSIGN) st a in BASSIGN holds
( s |= a iff a in (Label_ BASSIGN) . s )
let R be total Relation of S,S; :: thesis: for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for a being Assign of (CTLModel R,BASSIGN) st a in BASSIGN holds
( s |= a iff a in (Label_ BASSIGN) . s )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for a being Assign of (CTLModel R,BASSIGN) st a in BASSIGN holds
( s |= a iff a in (Label_ BASSIGN) . s )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for a being Assign of (CTLModel R,BASSIGN) st a in BASSIGN holds
( s |= a iff a in (Label_ BASSIGN) . s )
let a be Assign of (CTLModel R,BASSIGN); :: thesis: ( a in BASSIGN implies ( s |= a iff a in (Label_ BASSIGN) . s ) )
assume A1: a in BASSIGN ; :: thesis: ( s |= a iff a in (Label_ BASSIGN) . s )
thus ( s |= a implies a in (Label_ BASSIGN) . s ) :: thesis: ( a in (Label_ BASSIGN) . s implies s |= a )

proof

assume A2: s |= a ; :: thesis: a in (Label_ BASSIGN) . s
set f = Fid a,S;
A3: a = Fid a,S by Def41;
(Fid a,S) . s = TRUE by A2, Def59;
then a in F_LABEL s,BASSIGN by A1, A3, Def55;
hence a in (Label_ BASSIGN) . s by Def56; :: thesis: verum

end;

assume a in (Label_ BASSIGN) . s ; :: thesis: s |= a
then a in F_LABEL s,BASSIGN by Def56;
then consider f being Function of S,BOOLEAN such that
A4: f = a and
A5: f . s = TRUE by Def55;
Fid a,S = f by A4, Def41;
hence s |= a by A5, Def59; :: thesis: verum