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