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, g1, g2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= g1 holds
s |= g2 ) holds
for s being Element of S st s |= Fax (f,g1) holds
s |= Fax (f,g2)
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g1, g2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= g1 holds
s |= g2 ) holds
for s being Element of S st s |= Fax (f,g1) holds
s |= Fax (f,g2)
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g1, g2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= g1 holds
s |= g2 ) holds
for s being Element of S st s |= Fax (f,g1) holds
s |= Fax (f,g2)
let f, g1, g2 be Assign of (BASSModel (R,BASSIGN)); :: thesis: ( ( for s being Element of S st s |= g1 holds
s |= g2 ) implies for s being Element of S st s |= Fax (f,g1) holds
s |= Fax (f,g2) )
assume A1: for s being Element of S st s |= g1 holds
s |= g2 ; :: thesis: for s being Element of S st s |= Fax (f,g1) holds
s |= Fax (f,g2)
let s be Element of S; :: thesis: ( s |= Fax (f,g1) implies s |= Fax (f,g2) )
assume A2: s |= Fax (f,g1) ; :: thesis: s |= Fax (f,g2)
then s |= EX g1 by Th13;
then consider pai being inf_path of R such that
A3: pai . 0 = s and
A4: pai . 1 |= g1 by Th14;
pai . 1 |= g2 by A1, A4;
then A5: s |= EX g2 by A3, Th14;
s |= f by A2, Th13;
hence s |= Fax (f,g2) by A5, Th13; :: thesis: verum