let S be non empty set ; for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (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; for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (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); for f, g being Assign of (BASSModel (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 (BASSModel (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 H1, H2 be Subset of S; ( H1 c= H2 implies SigFoaxTau (g,f,H1,R,BASSIGN) c= SigFoaxTau (g,f,H2,R,BASSIGN) )
assume
H1 c= H2
; 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; verum