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 f1, f2 being Assign of (CTLModel R,BASSIGN) st ( for s being Element of S st s |= f1 holds
s |= f2 ) holds
SIGMA f1 c= SIGMA f2
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f1, f2 being Assign of (CTLModel R,BASSIGN) st ( for s being Element of S st s |= f1 holds
s |= f2 ) holds
SIGMA f1 c= SIGMA f2
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f1, f2 being Assign of (CTLModel R,BASSIGN) st ( for s being Element of S st s |= f1 holds
s |= f2 ) holds
SIGMA f1 c= SIGMA f2
let f1, f2 be Assign of (CTLModel R,BASSIGN); :: thesis: ( ( for s being Element of S st s |= f1 holds
s |= f2 ) implies SIGMA f1 c= SIGMA f2 )
assume A1: for s being Element of S st s |= f1 holds
s |= f2 ; :: thesis: SIGMA f1 c= SIGMA f2
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SIGMA f1 or x in SIGMA f2 )
assume x in SIGMA f1 ; :: thesis: x in SIGMA f2
then consider s being Element of S such that
A2: x = s and
A3: s |= f1 ;
s |= f2 by A1, A3;
hence x in SIGMA f2 by A2; :: thesis: verum