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 being Assign of (BASSModel (R,BASSIGN))
for G1, G2 being Subset of S st G1 c= G2 holds
SigFaxTau (f,G1,R,BASSIGN) c= SigFaxTau (f,G2,R,BASSIGN)
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN))
for G1, G2 being Subset of S st G1 c= G2 holds
SigFaxTau (f,G1,R,BASSIGN) c= SigFaxTau (f,G2,R,BASSIGN)
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (BASSModel (R,BASSIGN))
for G1, G2 being Subset of S st G1 c= G2 holds
SigFaxTau (f,G1,R,BASSIGN) c= SigFaxTau (f,G2,R,BASSIGN)
let f be Assign of (BASSModel (R,BASSIGN)); :: thesis: for G1, G2 being Subset of S st G1 c= G2 holds
SigFaxTau (f,G1,R,BASSIGN) c= SigFaxTau (f,G2,R,BASSIGN)
let G1, G2 be Subset of S; :: thesis: ( G1 c= G2 implies SigFaxTau (f,G1,R,BASSIGN) c= SigFaxTau (f,G2,R,BASSIGN) )
assume G1 c= G2 ; :: thesis: SigFaxTau (f,G1,R,BASSIGN) c= SigFaxTau (f,G2,R,BASSIGN)
then for s being Element of S st s |= Tau (G1,R,BASSIGN) holds
s |= Tau (G2,R,BASSIGN) by Th34;
then for s being Element of S st s |= Fax (f,(Tau (G1,R,BASSIGN))) holds
s |= Fax (f,(Tau (G2,R,BASSIGN))) by Th36;
hence SigFaxTau (f,G1,R,BASSIGN) c= SigFaxTau (f,G2,R,BASSIGN) by Th35; :: thesis: verum