let S be non empty set ; 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; 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); 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; ( 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
; for s being Element of S st s |= Tau (G1,R,BASSIGN) holds
s |= Tau (G2,R,BASSIGN)
let s be Element of S; ( s |= Tau (G1,R,BASSIGN) implies s |= Tau (G2,R,BASSIGN) )
assume
s |= Tau (G1,R,BASSIGN)
; s |= Tau (G2,R,BASSIGN)
then
(Fid ((Tau (G1,R,BASSIGN)),S)) . s = TRUE
;
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)
; verum