let S be non empty set ; :: thesis: for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (CTLModel R,BASSIGN)
for H1, H2 being Subset of S st H1 c= H2 holds
SigFoaxTau g,f,H1,R,BASSIGN c= SigFoaxTau g,f,H2,R,BASSIGN
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (CTLModel R,BASSIGN)
for H1, H2 being Subset of S 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 (ModelSP S); :: thesis: for f, g being Assign of (CTLModel R,BASSIGN)
for H1, H2 being Subset of S 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 S st H1 c= H2 holds
SigFoaxTau g,f,H1,R,BASSIGN c= SigFoaxTau g,f,H2,R,BASSIGN
let H1, H2 be Subset of S; :: 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