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 (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; :: thesis: 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); :: thesis: 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)); :: 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