let S be non empty set ; :: thesis: for R being total Relation of ,
for BASSIGN being non empty Subset of
for f, g being Assign of (CTLModel R,BASSIGN)
for H1, H2 being Subset of st H1 c= H2 holds
SigFoaxTau g,f,H1,R,BASSIGN c= SigFoaxTau g,f,H2,R,BASSIGN
let R be total Relation of ,; :: thesis: for BASSIGN being non empty Subset of
for f, g being Assign of (CTLModel R,BASSIGN)
for H1, H2 being Subset of st H1 c= H2 holds
SigFoaxTau g,f,H1,R,BASSIGN c= SigFoaxTau g,f,H2,R,BASSIGN
let BASSIGN be non empty Subset of ; :: thesis: for f, g being Assign of (CTLModel R,BASSIGN)
for H1, H2 being Subset of st H1 c= H2 holds
SigFoaxTau g,f,H1,R,BASSIGN c= SigFoaxTau g,f,H2,R,BASSIGN
let f, g be Assign of (CTLModel R,BASSIGN); :: thesis: for H1, H2 being Subset of st H1 c= H2 holds
SigFoaxTau g,f,H1,R,BASSIGN c= SigFoaxTau g,f,H2,R,BASSIGN
let H1, H2 be Subset of ; :: thesis: ( H1 c= H2 implies SigFoaxTau g,f,H1,R,BASSIGN c= SigFoaxTau g,f,H2,R,BASSIGN )
assume H1 c= H2 ; :: thesis: SigFoaxTau g,f,H1,R,BASSIGN c= SigFoaxTau g,f,H2,R,BASSIGN
then for s being Element of S st s |= Tau H1,R,BASSIGN holds
s |= Tau H2,R,BASSIGN by Th34;
then for s being Element of S st s |= Foax g,f,(Tau H1,R,BASSIGN) holds
s |= Foax g,f,(Tau H2,R,BASSIGN) by Th44;
hence SigFoaxTau g,f,H1,R,BASSIGN c= SigFoaxTau g,f,H2,R,BASSIGN by Th35; :: thesis: verum