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 G1, G2 being Subset of S st G1 c= G2 holds
for s being Element of S st s |= Tau G1,R,BASSIGN holds
s |= Tau G2,R,BASSIGN
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for G1, G2 being Subset of S st G1 c= G2 holds
for s being Element of S st s |= Tau G1,R,BASSIGN holds
s |= Tau G2,R,BASSIGN
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for G1, G2 being Subset of S st G1 c= G2 holds
for s being Element of S st s |= Tau G1,R,BASSIGN holds
s |= Tau G2,R,BASSIGN
let G1, G2 be Subset of S; :: thesis: ( G1 c= G2 implies for s being Element of S st s |= Tau G1,R,BASSIGN holds
s |= Tau G2,R,BASSIGN )
set Tau1 = Tau G1,R,BASSIGN;
set Tau2 = Tau G2,R,BASSIGN;
assume A1: G1 c= G2 ; :: thesis: for s being Element of S st s |= Tau G1,R,BASSIGN holds
s |= Tau G2,R,BASSIGN
let s be Element of S; :: thesis: ( s |= Tau G1,R,BASSIGN implies s |= Tau G2,R,BASSIGN )
assume s |= Tau G1,R,BASSIGN ; :: thesis: s |= Tau G2,R,BASSIGN
then (Fid (Tau G1,R,BASSIGN),S) . s = TRUE by Def59;
then (chi G1,S) . s = 1 by Def64;
then s in G1 by FUNCT_3:def 3;
then (chi G2,S) . s = 1 by A1, FUNCT_3:def 3;
then (Fid (Tau G2,R,BASSIGN),S) . s = TRUE by Def64;
hence s |= Tau G2,R,BASSIGN by Def59; :: thesis: verum